Loogle!
Result
Found 243 definitions mentioning List and Fin. Of these, only the first 200 are shown.
- List.get Init.Prelude
{α : Type u} → (as : List α) → Fin as.length → α - List.sizeOf_get Init.Data.List.BasicAux
∀ {α : Type u_1} [inst : SizeOf α] (as : List α) (i : Fin as.length), sizeOf (as.get i) < sizeOf as - List.get_last Init.Data.List.BasicAux
∀ {α : Type u_1} {a : α} {as : List α} {i : Fin (as ++ [a]).length}, ¬↑i < as.length → (as ++ [a]).get i = a - List.get_cons_succ' Init.Data.List.Lemmas
∀ {α : Type u_1} {a : α} {as : List α} {i : Fin as.length}, (a :: as).get i.succ = as.get i - List.get_of_mem Init.Data.List.Lemmas
∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l → ∃ n, l.get n = a - List.mem_iff_get Init.Data.List.Lemmas
∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l ↔ ∃ n, l.get n = a - List.get_cons_zero Init.Data.List.Lemmas
∀ {α : Type u_1} {a : α} {l : List α}, (a :: l).get 0 = a - List.get_eq_getElem Init.Data.List.Lemmas
∀ {α : Type u_1} (l : List α) (i : Fin l.length), l.get i = l[↑i] - List.get_cons_cons_one Init.Data.List.Lemmas
∀ {α : Type u_1} {a₁ a₂ : α} {as : List α}, (a₁ :: a₂ :: as).get 1 = a₂ - List.get_of_eq Init.Data.List.Lemmas
∀ {α : Type u_1} {l l' : List α} (h : l = l') (i : Fin l.length), l.get i = l'.get ⟨↑i, ⋯⟩ - List.get_map Init.Data.List.Lemmas
∀ {α : Type u_1} {β : Type u_2} (f : α → β) {l : List α} {n : Fin (List.map f l).length}, (List.map f l).get n = f (l.get ⟨↑n, ⋯⟩) - List.get_dropLast Init.Data.List.Lemmas
∀ {α : Type u_1} (xs : List α) (i : Fin xs.dropLast.length), xs.dropLast.get i = xs.get ⟨↑i, ⋯⟩ - List.get_cons_drop Init.Data.List.TakeDrop
∀ {α : Type u_1} (l : List α) (i : Fin l.length), l.get i :: List.drop (↑i + 1) l = List.drop (↑i) l - List.get_take' Init.Data.List.Nat.TakeDrop
∀ {α : Type u_1} (L : List α) {j : ℕ} {i : Fin (List.take j L).length}, (List.take j L).get i = L.get ⟨↑i, ⋯⟩ - List.get_drop' Init.Data.List.Nat.TakeDrop
∀ {α : Type u_1} (L : List α) {i : ℕ} {j : Fin (List.drop i L).length}, (List.drop i L).get j = L.get ⟨i + ↑j, ⋯⟩ - Array.data_set Init.Data.Array.Lemmas
∀ {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α), (a.set i v).data = a.data.set (↑i) v - Array.data_swap Init.Data.Array.Lemmas
∀ {α : Type u_1} (a : Array α) (i j : Fin a.size), (a.swap i j).data = (a.data.set (↑i) (a.get j)).set (↑j) (a.get i) - List.map_get_sublist Init.Data.List.Nat.Pairwise
∀ {α : Type u_1} {l : List α} {is : List (Fin l.length)}, List.Pairwise (fun x1 x2 => ↑x1 < ↑x2) is → (List.map l.get is).Sublist l - List.sublist_eq_map_get Init.Data.List.Nat.Pairwise
∀ {α : Type u_1} {l' l : List α}, l'.Sublist l → ∃ is, l' = List.map l.get is ∧ List.Pairwise (fun x1 x2 => x1 < x2) is - List.map_getElem_sublist Init.Data.List.Nat.Pairwise
∀ {α : Type u_1} {l : List α} {is : List (Fin l.length)}, List.Pairwise (fun x1 x2 => x1 < x2) is → (List.map (fun x => l[x]) is).Sublist l - List.sublist_eq_map_getElem Init.Data.List.Nat.Pairwise
∀ {α : Type u_1} {l l' : List α}, l'.Sublist l → ∃ is, l' = List.map (fun x => l[x]) is ∧ List.Pairwise (fun x1 x2 => x1 < x2) is - List.ofFn Batteries.Data.List.Basic
{α : Type u_1} → {n : ℕ} → (Fin n → α) → List α - List.ofFnTR Batteries.Data.List.Basic
{α : Type u_1} → {n : ℕ} → (Fin n → α) → List α - List.ofFn_eq_ofFnTR Batteries.Data.List.Basic
@List.ofFn = @List.ofFnTR - List.ofFnTR.go Batteries.Data.List.Basic
{α : Type u_1} → {n : ℕ} → (Fin n → α) → (i : ℕ) → i ≤ n → List α → List α - List.ofFn.go Batteries.Data.List.Basic
{α : Type u_1} → {n : ℕ} → (Fin n → α) → (i j : ℕ) → i + j = n → List α - List.ofFnTR.eq_1 Batteries.Data.List.Basic
∀ {α : Type u_1} {n : ℕ} (f : Fin n → α), List.ofFnTR f = List.ofFnTR.go f n ⋯ [] - List.ofFnTR.go.eq_1 Batteries.Data.List.Basic
∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (x : List α) (x_3 : 0 ≤ n), List.ofFnTR.go f 0 x_3 x = x - List.ofFn_eq_ofFnTR.go Batteries.Data.List.Basic
∀ (α : Type u_1) (n : ℕ) (f : Fin n → α) (i j : ℕ) (h : i + j = n) (h' : j ≤ n), List.ofFnTR.go f j h' (List.ofFn.go f i j h) = List.ofFn f - List.ofFnTR.go.eq_2 Batteries.Data.List.Basic
∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (x : List α) (i : ℕ) (h : i + 1 ≤ n), List.ofFnTR.go f i.succ h x = List.ofFnTR.go f i ⋯ (f ⟨i, h⟩ :: x) - List.ofFnTR.go.eq_def Batteries.Data.List.Basic
∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (x : ℕ) (x_1 : x ≤ n) (x_2 : List α), List.ofFnTR.go f x x_1 x_2 = match x, x_1, x_2 with | 0, x, acc => acc | i.succ, h, acc => List.ofFnTR.go f i ⋯ (f ⟨i, h⟩ :: acc) - List.get_eq_iff Batteries.Data.List.Lemmas
∀ {α : Type u_1} {l : List α} {n : Fin l.length} {x : α}, l.get n = x ↔ l.get? ↑n = some x - Fin.list Batteries.Data.Fin.Basic
(n : ℕ) → List (Fin n) - Fin.list.eq_1 Batteries.Data.Fin.Lemmas
∀ (n : ℕ), Fin.list n = (Fin.enum n).data - Fin.list_reverse Batteries.Data.Fin.Lemmas
∀ (n : ℕ), (Fin.list n).reverse = List.map Fin.rev (Fin.list n) - Fin.list_zero Batteries.Data.Fin.Lemmas
Fin.list 0 = [] - Fin.list_succ Batteries.Data.Fin.Lemmas
∀ (n : ℕ), Fin.list (n + 1) = 0 :: List.map Fin.succ (Fin.list n) - Fin.getElem_list Batteries.Data.Fin.Lemmas
∀ {n : ℕ} (i : ℕ) (h : i < (Fin.list n).length), (Fin.list n)[i] = Fin.cast ⋯ ⟨i, h⟩ - Fin.list_succ_last Batteries.Data.Fin.Lemmas
∀ (n : ℕ), Fin.list (n + 1) = List.map Fin.castSucc (Fin.list n) ++ [Fin.last n] - List.mem_eraseIdx_iff_get Batteries.Data.List.EraseIdx
∀ {α : Type u} {x : α} {l : List α} {k : ℕ}, x ∈ l.eraseIdx k ↔ ∃ i, ↑i ≠ k ∧ l.get i = x - List.pairwise_iff_get Batteries.Data.List.Pairwise
∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.Pairwise R l ↔ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j) - Batteries.Linter.UnnecessarySeqFocus.getPath Batteries.Linter.UnnecessarySeqFocus
Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List ((n : ℕ) × Fin n) → Option Lean.Elab.Info - Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.existsRatHint_of_ratHintsExhaustive Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n), f.ReadyForRatAdd → ∀ (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHints : Array (ℕ × Array ℕ)), f.ratHintsExhaustive pivot ratHints = true → ∀ c' ∈ f.toList, pivot.negate ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c' → ∃ i, f.clauses[ratHints[i].1]! = some c' - List.erase_get Mathlib.Data.List.Basic
∀ {ι : Type u_1} [inst : DecidableEq ι] {l : List ι} (i : Fin l.length), (l.erase (l.get i)).Perm (l.eraseIdx ↑i) - List.cons_get_drop_succ Mathlib.Data.List.Basic
∀ {α : Type u} {l : List α} {n : Fin l.length}, l.get n :: List.drop (↑n + 1) l = List.drop (↑n) l - List.get_map_rev Mathlib.Data.List.Basic
∀ {α : Type u} {β : Type v} (f : α → β) {l : List α} {n : Fin l.length}, f (l.get n) = (List.map f l).get ⟨↑n, ⋯⟩ - List.get_reverse' Mathlib.Data.List.Basic
∀ {α : Type u} (l : List α) (n : Fin l.reverse.length) (hn' : l.length - 1 - ↑n < l.length), l.reverse.get n = l.get ⟨l.length - 1 - ↑n, hn'⟩ - List.get_attach Mathlib.Data.List.Basic
∀ {α : Type u} (L : List α) (i : Fin L.attach.length), ↑(L.attach.get i) = L.get ⟨↑i, ⋯⟩ - List.get_eq_get? Mathlib.Data.List.Basic
∀ {α : Type u} (l : List α) (i : Fin l.length), l.get i = (l.get? ↑i).get ⋯ - List.nodup_iff_injective_get Mathlib.Data.List.Nodup
∀ {α : Type u} {l : List α}, l.Nodup ↔ Function.Injective l.get - List.get_indexOf Mathlib.Data.List.Nodup
∀ {α : Type u} [inst : DecidableEq α] {l : List α}, l.Nodup → ∀ (i : Fin l.length), List.indexOf (l.get i) l = ↑i - List.not_nodup_of_get_eq_of_ne Mathlib.Data.List.Nodup
∀ {α : Type u} (xs : List α) (n m : Fin xs.length), xs.get n = xs.get m → n ≠ m → ¬xs.Nodup - List.Nodup.get_inj_iff Mathlib.Data.List.Nodup
∀ {α : Type u} {l : List α}, l.Nodup → ∀ {i j : Fin l.length}, l.get i = l.get j ↔ i = j - List.Nodup.erase_get Mathlib.Data.List.Nodup
∀ {α : Type u} [inst : DecidableEq α] {l : List α}, l.Nodup → ∀ (i : Fin l.length), l.erase (l.get i) = l.eraseIdx ↑i - List.nodup_iff_injective_getElem Mathlib.Data.List.Nodup
∀ {α : Type u} {l : List α}, l.Nodup ↔ Function.Injective fun i => l[↑i] - List.drop_take_succ_eq_cons_get Mathlib.Data.List.Join
∀ {α : Type u_1} (L : List α) (i : Fin L.length), List.drop (↑i) (List.take (↑i + 1) L) = [L.get i] - List.drop_take_succ_join_eq_get' Mathlib.Data.List.Join
∀ {α : Type u_1} (L : List (List α)) (i : Fin L.length), List.drop (Nat.sum (List.take (↑i) (List.map List.length L))) (List.take (Nat.sum (List.take (↑i + 1) (List.map List.length L))) L.join) = L.get i - Set.range_list_get Mathlib.Data.Set.List
∀ {α : Type u_1} (l : List α), Set.range l.get = {x | x ∈ l} - Set.range_list_nthLe Mathlib.Data.Set.List
∀ {α : Type u_1} (l : List α), Set.range l.get = {x | x ∈ l} - List.get_inits Mathlib.Data.List.Infix
∀ {α : Type u_1} (l : List α) (n : Fin l.inits.length), l.inits.get n = List.take (↑n) l - List.get_tails Mathlib.Data.List.Infix
∀ {α : Type u_1} (l : List α) (n : Fin l.tails.length), l.tails.get n = List.drop (↑n) l - List.finRange Mathlib.Data.List.Range
(n : ℕ) → List (Fin n) - List.mem_finRange Mathlib.Data.List.Range
∀ {n : ℕ} (a : Fin n), a ∈ List.finRange n - List.finRange_eq_nil Mathlib.Data.List.Range
∀ {n : ℕ}, List.finRange n = [] ↔ n = 0 - List.finRange_map_get Mathlib.Data.List.Range
∀ {α : Type u} (l : List α), List.map l.get (List.finRange l.length) = l - List.finRange_zero Mathlib.Data.List.Range
List.finRange 0 = [] - List.finRange.eq_1 Mathlib.Data.List.Range
∀ (n : ℕ), List.finRange n = List.pmap Fin.mk (List.range n) ⋯ - List.getElem_finRange Mathlib.Data.List.Range
∀ {n i : ℕ} (h : i < (List.finRange n).length), (List.finRange n)[i] = ⟨i, ⋯⟩ - List.get_cyclicPermutations Mathlib.Data.List.Rotate
∀ {α : Type u} (l : List α) (n : Fin l.cyclicPermutations.length), l.cyclicPermutations.get n = l.rotate ↑n - List.get_rotate Mathlib.Data.List.Rotate
∀ {α : Type u} (l : List α) (n : ℕ) (k : Fin (l.rotate n).length), (l.rotate n).get k = l.get ⟨(↑k + n) % l.length, ⋯⟩ - List.get_rotate_one Mathlib.Data.List.Rotate
∀ {α : Type u} (l : List α) (k : Fin (l.rotate 1).length), (l.rotate 1).get k = l.get ⟨(↑k + 1) % l.length, ⋯⟩ - List.nthLe_rotate_one Mathlib.Data.List.Rotate
∀ {α : Type u} (l : List α) (k : Fin (l.rotate 1).length), (l.rotate 1).get k = l.get ⟨(↑k + 1) % l.length, ⋯⟩ - List.get_eq_get_rotate Mathlib.Data.List.Rotate
∀ {α : Type u} (l : List α) (n : ℕ) (k : Fin l.length), l.get k = (l.rotate n).get ⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩ - List.drop_take_succ_join_eq_get Mathlib.Algebra.BigOperators.Group.List
∀ {α : Type u_2} (L : List (List α)) (i : Fin L.length), List.drop (List.take (↑i) (List.map List.length L)).sum (List.take (List.take (↑i + 1) (List.map List.length L)).sum L.join) = L.get i - List.equivSigmaTuple Mathlib.Data.List.OfFn
{α : Type u} → List α ≃ (n : ℕ) × (Fin n → α) - List.ofFn_injective Mathlib.Data.List.OfFn
∀ {α : Type u} {n : ℕ}, Function.Injective List.ofFn - List.ofFn_const Mathlib.Data.List.OfFn
∀ {α : Type u} (n : ℕ) (c : α), (List.ofFn fun x => c) = List.replicate n c - List.ofFnRec Mathlib.Data.List.OfFn
{α : Type u} → {C : List α → Sort u_1} → ((n : ℕ) → (f : Fin n → α) → C (List.ofFn f)) → (l : List α) → C l - List.forall_iff_forall_tuple Mathlib.Data.List.OfFn
∀ {α : Type u} {P : List α → Prop}, (∀ (l : List α), P l) ↔ ∀ (n : ℕ) (f : Fin n → α), P (List.ofFn f) - List.ofFn_zero Mathlib.Data.List.OfFn
∀ {α : Type u} (f : Fin 0 → α), List.ofFn f = [] - List.ofFn_eq_nil_iff Mathlib.Data.List.OfFn
∀ {α : Type u} {n : ℕ} {f : Fin n → α}, List.ofFn f = [] ↔ n = 0 - List.ofFn.eq_1 Mathlib.Data.List.OfFn
∀ {α : Type u_1} {n : ℕ} (f : Fin n → α), List.ofFn f = List.ofFn.go f n 0 ⋯ - List.ofFn_inj Mathlib.Data.List.OfFn
∀ {α : Type u} {n : ℕ} {f g : Fin n → α}, List.ofFn f = List.ofFn g ↔ f = g - List.exists_iff_exists_tuple Mathlib.Data.List.OfFn
∀ {α : Type u} {P : List α → Prop}, (∃ l, P l) ↔ ∃ n f, P (List.ofFn f) - List.forall_mem_ofFn_iff Mathlib.Data.List.OfFn
∀ {α : Type u} {n : ℕ} {f : Fin n → α} {P : α → Prop}, (∀ i ∈ List.ofFn f, P i) ↔ ∀ (j : Fin n), P (f j) - List.ofFn_get_eq_map Mathlib.Data.List.OfFn
∀ {α : Type u} {β : Type u_1} (l : List α) (f : α → β), (List.ofFn fun x => f (l.get x)) = List.map f l - List.ofFn_succ' Mathlib.Data.List.OfFn
∀ {α : Type u} {n : ℕ} (f : Fin n.succ → α), List.ofFn f = (List.ofFn fun i => f i.castSucc).concat (f (Fin.last n)) - List.map_ofFn Mathlib.Data.List.OfFn
∀ {α : Type u} {β : Type u_1} {n : ℕ} (f : Fin n → α) (g : α → β), List.map g (List.ofFn f) = List.ofFn (g ∘ f) - List.mem_ofFn Mathlib.Data.List.OfFn
∀ {α : Type u} {n : ℕ} (f : Fin n → α) (a : α), a ∈ List.ofFn f ↔ a ∈ Set.range f - List.ofFn_congr Mathlib.Data.List.OfFn
∀ {α : Type u} {m n : ℕ} (h : m = n) (f : Fin m → α), List.ofFn f = List.ofFn fun i => f (Fin.cast ⋯ i) - List.ofFnRec_ofFn Mathlib.Data.List.OfFn
∀ {α : Type u} {C : List α → Sort u_1} (h : (n : ℕ) → (f : Fin n → α) → C (List.ofFn f)) {n : ℕ} (f : Fin n → α), List.ofFnRec h (List.ofFn f) = h n f - List.ofFn_fin_repeat Mathlib.Data.List.OfFn
∀ {α : Type u} {m : ℕ} (a : Fin m → α) (n : ℕ), List.ofFn (Fin.repeat n a) = (List.replicate n (List.ofFn a)).join - List.ofFn_succ Mathlib.Data.List.OfFn
∀ {α : Type u} {n : ℕ} (f : Fin n.succ → α), List.ofFn f = f 0 :: List.ofFn fun i => f i.succ - List.ofFn.go.eq_1 Mathlib.Data.List.OfFn
∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (x : ℕ) (x_1 : 0 + x = n), List.ofFn.go f 0 x x_1 = [] - List.ofFn_inj' Mathlib.Data.List.OfFn
∀ {α : Type u} {m n : ℕ} {f : Fin m → α} {g : Fin n → α}, List.ofFn f = List.ofFn g ↔ ⟨m, f⟩ = ⟨n, g⟩ - List.equivSigmaTuple_apply_fst Mathlib.Data.List.OfFn
∀ {α : Type u} (l : List α), (List.equivSigmaTuple l).fst = l.length - List.ofFnRec.eq_1 Mathlib.Data.List.OfFn
∀ {α : Type u} {C : List α → Sort u_1} (h : (n : ℕ) → (f : Fin n → α) → C (List.ofFn f)) (l : List α), List.ofFnRec h l = cast ⋯ (h l.length l.get) - List.ofFn_fin_append Mathlib.Data.List.OfFn
∀ {α : Type u} {m n : ℕ} (a : Fin m → α) (b : Fin n → α), List.ofFn (Fin.append a b) = List.ofFn a ++ List.ofFn b - List.equivSigmaTuple_apply_snd Mathlib.Data.List.OfFn
∀ {α : Type u} (l : List α) (a : Fin l.length), (List.equivSigmaTuple l).snd a = l.get a - List.getElem?_ofFn Mathlib.Data.List.OfFn
∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i : ℕ), (List.ofFn f)[i]? = List.ofFnNthVal f i - List.ofFn_add Mathlib.Data.List.OfFn
∀ {α : Type u} {m n : ℕ} (f : Fin (m + n) → α), List.ofFn f = (List.ofFn fun i => f (Fin.castAdd n i)) ++ List.ofFn fun j => f (Fin.natAdd m j) - List.ofFn_getElem Mathlib.Data.List.OfFn
∀ {α : Type u} (l : List α), (List.ofFn fun i => l[↑i]) = l - List.ofFn.go.eq_2 Mathlib.Data.List.OfFn
∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (x i : ℕ) (x_1 : i.succ + x = n), List.ofFn.go f i.succ x x_1 = f ⟨x, ⋯⟩ :: List.ofFn.go f i (x + 1) ⋯ - List.ofFn_getElem_eq_map Mathlib.Data.List.OfFn
∀ {α : Type u} {β : Type u_1} (l : List α) (f : α → β), (List.ofFn fun i => f l[↑i]) = List.map f l - List.equivSigmaTuple_symm_apply Mathlib.Data.List.OfFn
∀ {α : Type u} (f : (n : ℕ) × (Fin n → α)), List.equivSigmaTuple.symm f = List.ofFn f.snd - List.last_ofFn_succ Mathlib.Data.List.OfFn
∀ {α : Type u} {n : ℕ} (f : Fin n.succ → α) (h : optParam (List.ofFn f ≠ []) ⋯), (List.ofFn f).getLast h = f (Fin.last n) - List.getElem_ofFn Mathlib.Data.List.OfFn
∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i : ℕ) (h : i < (List.ofFn f).length), (List.ofFn f)[i] = f ⟨i, ⋯⟩ - List.last_ofFn Mathlib.Data.List.OfFn
∀ {α : Type u} {n : ℕ} (f : Fin n → α) (h : List.ofFn f ≠ []) (hn : optParam (n - 1 < n) ⋯), (List.ofFn f).getLast h = f ⟨n - 1, hn⟩ - List.ofFn_mul Mathlib.Data.List.OfFn
∀ {α : Type u} {m n : ℕ} (f : Fin (m * n) → α), List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).join - List.ofFn_mul' Mathlib.Data.List.OfFn
∀ {α : Type u} {m n : ℕ} (f : Fin (m * n) → α), List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨m * ↑i + ↑j, ⋯⟩).join - List.getElem_ofFn_go Mathlib.Data.List.OfFn
∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i j : ℕ) (h : i + j = n) (k : ℕ) (hk : k < (List.ofFn.go f i j h).length), (List.ofFn.go f i j h)[k] = f ⟨j + k, ⋯⟩ - List.map_coe_finRange Mathlib.Data.List.FinRange
∀ (n : ℕ), List.map Fin.val (List.finRange n) = List.range n - List.ofFn_id Mathlib.Data.List.FinRange
∀ (n : ℕ), List.ofFn id = List.finRange n - List.ofFn_eq_map Mathlib.Data.List.FinRange
∀ {α : Type u} {n : ℕ} {f : Fin n → α}, List.ofFn f = List.map f (List.finRange n) - List.finRange_succ_eq_map Mathlib.Data.List.FinRange
∀ (n : ℕ), List.finRange n.succ = 0 :: List.map Fin.succ (List.finRange n) - List.finRange_succ Mathlib.Data.List.FinRange
∀ (n : ℕ), List.finRange n.succ = (List.map Fin.castSucc (List.finRange n)).concat (Fin.last n) - List.ofFn_eq_pmap Mathlib.Data.List.FinRange
∀ {α : Type u} {n : ℕ} {f : Fin n → α}, List.ofFn f = List.pmap (fun i hi => f ⟨i, hi⟩) (List.range n) ⋯ - Fin.univ_image_get Mathlib.Data.Fintype.Basic
∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), Finset.image l.get Finset.univ = l.toFinset - Fin.univ_image_get' Mathlib.Data.Fintype.Basic
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (l : List α) (f : α → β), Finset.image (fun x => f (l.get x)) Finset.univ = (List.map f l).toFinset - Fin.univ_image_getElem' Mathlib.Data.Fintype.Basic
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (l : List α) (f : α → β), Finset.image (fun i => f l[↑i]) Finset.univ = (List.map f l).toFinset - List.Sorted.rel_get_of_lt Mathlib.Data.List.Sort
∀ {α : Type u} {r : α → α → Prop} {l : List α}, List.Sorted r l → ∀ {a b : Fin l.length}, a < b → r (l.get a) (l.get b) - List.Sorted.rel_get_of_le Mathlib.Data.List.Sort
∀ {α : Type u} {r : α → α → Prop} [inst : IsRefl α r] {l : List α}, List.Sorted r l → ∀ {a b : Fin l.length}, a ≤ b → r (l.get a) (l.get b) - List.Nodup.getEquivOfForallMemList Mathlib.Data.List.NodupEquivFin
{α : Type u_1} → [inst : DecidableEq α] → (l : List α) → l.Nodup → (∀ (x : α), x ∈ l) → Fin l.length ≃ α - List.Nodup.getEquiv Mathlib.Data.List.NodupEquivFin
{α : Type u_1} → [inst : DecidableEq α] → (l : List α) → l.Nodup → Fin l.length ≃ { x // x ∈ l } - List.Nodup.getBijectionOfForallMemList Mathlib.Data.List.NodupEquivFin
{α : Type u_1} → (l : List α) → l.Nodup → (∀ (x : α), x ∈ l) → { f // Function.Bijective f } - List.Sorted.get_mono Mathlib.Data.List.NodupEquivFin
∀ {α : Type u_1} [inst : Preorder α] {l : List α}, List.Sorted (fun x1 x2 => x1 ≤ x2) l → Monotone l.get - List.Sorted.get_strictMono Mathlib.Data.List.NodupEquivFin
∀ {α : Type u_1} [inst : Preorder α] {l : List α}, List.Sorted (fun x1 x2 => x1 < x2) l → StrictMono l.get - List.Nodup.getBijectionOfForallMemList_coe Mathlib.Data.List.NodupEquivFin
∀ {α : Type u_1} (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (i : Fin l.length), ↑(List.Nodup.getBijectionOfForallMemList l nd h) i = l.get i - List.Sorted.getIso Mathlib.Data.List.NodupEquivFin
{α : Type u_1} → [inst : Preorder α] → [inst_1 : DecidableEq α] → (l : List α) → List.Sorted (fun x1 x2 => x1 < x2) l → Fin l.length ≃o { x // x ∈ l } - List.Nodup.getEquivOfForallMemList_apply Mathlib.Data.List.NodupEquivFin
∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (i : Fin l.length), (List.Nodup.getEquivOfForallMemList l nd h) i = l.get i - List.Nodup.getEquivOfForallMemList_symm_apply_val Mathlib.Data.List.NodupEquivFin
∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (a : α), ↑((List.Nodup.getEquivOfForallMemList l nd h).symm a) = List.indexOf a l - List.duplicate_iff_exists_distinct_get Mathlib.Data.List.NodupEquivFin
∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x l ↔ ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m - List.Nodup.getEquiv_apply_coe Mathlib.Data.List.NodupEquivFin
∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (H : l.Nodup) (i : Fin l.length), ↑((List.Nodup.getEquiv l H) i) = l.get i - List.Nodup.getEquiv_symm_apply_val Mathlib.Data.List.NodupEquivFin
∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (H : l.Nodup) (x : { x // x ∈ l }), ↑((List.Nodup.getEquiv l H).symm x) = List.indexOf (↑x) l - List.sublist_iff_exists_fin_orderEmbedding_get_eq Mathlib.Data.List.NodupEquivFin
∀ {α : Type u_1} {l l' : List α}, l.Sublist l' ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix) - List.Sorted.coe_getIso_apply Mathlib.Data.List.NodupEquivFin
∀ {α : Type u_1} [inst : Preorder α] {l : List α} [inst_1 : DecidableEq α] (H : List.Sorted (fun x1 x2 => x1 < x2) l) {i : Fin l.length}, ↑((List.Sorted.getIso l H) i) = l.get i - List.Sorted.coe_getIso_symm_apply Mathlib.Data.List.NodupEquivFin
∀ {α : Type u_1} [inst : Preorder α] {l : List α} [inst_1 : DecidableEq α] (H : List.Sorted (fun x1 x2 => x1 < x2) l) {x : { x // x ∈ l }}, ↑((List.Sorted.getIso l H).symm x) = List.indexOf (↑x) l - List.get_zip Mathlib.Data.List.Zip
∀ {α : Type u} {β : Type u_1} {l : List α} {l' : List β} {i : Fin (l.zip l').length}, (l.zip l').get i = (l.get ⟨↑i, ⋯⟩, l'.get ⟨↑i, ⋯⟩) - List.get_zipWith Mathlib.Data.List.Zip
∀ {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {l : List α} {l' : List β} {i : Fin (List.zipWith f l l').length}, (List.zipWith f l l').get i = f (l.get ⟨↑i, ⋯⟩) (l'.get ⟨↑i, ⋯⟩) - Mathlib.Vector.toList_ofFn Mathlib.Data.Vector.Basic
∀ {α : Type u_1} {n : ℕ} (f : Fin n → α), (Mathlib.Vector.ofFn f).toList = List.ofFn f - Mathlib.Vector.toList_set Mathlib.Data.Vector.Basic
∀ {α : Type u_1} {n : ℕ} (v : Mathlib.Vector α n) (i : Fin n) (a : α), (v.set i a).toList = v.toList.set (↑i) a - Mathlib.Vector.set.eq_1 Mathlib.Data.Vector.Basic
∀ {α : Type u_1} {n : ℕ} (v : Mathlib.Vector α n) (i : Fin n) (a : α), v.set i a = ⟨(↑v).set (↑i) a, ⋯⟩ - Mathlib.Vector.eraseIdx_val Mathlib.Data.Vector.Basic
∀ {α : Type u_1} {n : ℕ} {i : Fin n} {v : Mathlib.Vector α n}, ↑(Mathlib.Vector.eraseIdx i v) = (↑v).eraseIdx ↑i - Mathlib.Vector.removeNth_val Mathlib.Data.Vector.Basic
∀ {α : Type u_1} {n : ℕ} {i : Fin n} {v : Mathlib.Vector α n}, ↑(Mathlib.Vector.eraseIdx i v) = (↑v).eraseIdx ↑i - Mathlib.Vector.insertNth_val Mathlib.Data.Vector.Basic
∀ {α : Type u_1} {n : ℕ} {a : α} {i : Fin (n + 1)} {v : Mathlib.Vector α n}, ↑(Mathlib.Vector.insertNth a i v) = List.insertNth (↑i) a ↑v - Fin.prod_univ_get Mathlib.Algebra.BigOperators.Fin
∀ {α : Type u_1} [inst : CommMonoid α] (l : List α), ∏ i : Fin l.length, l[↑i] = l.prod - Fin.sum_univ_get Mathlib.Algebra.BigOperators.Fin
∀ {α : Type u_1} [inst : AddCommMonoid α] (l : List α), ∑ i : Fin l.length, l[↑i] = l.sum - Fin.prod_univ_get' Mathlib.Algebra.BigOperators.Fin
∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid β] (l : List α) (f : α → β), ∏ i : Fin l.length, f l[↑i] = (List.map f l).prod - Fin.sum_univ_get' Mathlib.Algebra.BigOperators.Fin
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid β] (l : List α) (f : α → β), ∑ i : Fin l.length, f l[↑i] = (List.map f l).sum - List.alternatingProd_eq_finset_prod Mathlib.Algebra.BigOperators.Fin
∀ {G : Type u_3} [inst : CommGroup G] (L : List G), L.alternatingProd = ∏ i : Fin L.length, L[i] ^ (-1) ^ ↑i - List.alternatingSum_eq_finset_sum Mathlib.Algebra.BigOperators.Fin
∀ {G : Type u_3} [inst : AddCommGroup G] (L : List G), L.alternatingSum = ∑ i : Fin L.length, (-1) ^ ↑i • L[i] - Fin.sort_univ Mathlib.Data.Finset.Sort
∀ (n : ℕ), Finset.sort (fun x y => x ≤ y) Finset.univ = List.finRange n - Finset.orderEmbOfFin_apply Mathlib.Data.Finset.Sort
∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k), (s.orderEmbOfFin h) i = (Finset.sort (fun x1 x2 => x1 ≤ x2) s)[i] - Composition.blocksFun_mem_blocks Mathlib.Combinatorics.Enumerative.Composition
∀ {n : ℕ} (c : Composition n) (i : Fin c.length), c.blocksFun i ∈ c.blocks - Composition.blocksFun_congr Mathlib.Combinatorics.Enumerative.Composition
∀ {n₁ n₂ : ℕ} (c₁ : Composition n₁) (c₂ : Composition n₂) (i₁ : Fin c₁.length) (i₂ : Fin c₂.length), n₁ = n₂ → c₁.blocks = c₂.blocks → ↑i₁ = ↑i₂ → c₁.blocksFun i₁ = c₂.blocksFun i₂ - List.get_splitWrtComposition Mathlib.Combinatorics.Enumerative.Composition
∀ {n : ℕ} {α : Type u_1} (l : List α) (c : Composition n) (i : Fin (l.splitWrtComposition c).length), (l.splitWrtComposition c).get i = List.drop (c.sizeUpTo ↑i) (List.take (c.sizeUpTo (↑i + 1)) l) - List.formPerm_apply_get Mathlib.GroupTheory.Perm.List
∀ {α : Type u_1} [inst : DecidableEq α] (xs : List α), xs.Nodup → ∀ (i : Fin xs.length), xs.formPerm (xs.get i) = xs.get ⟨(↑i + 1) % xs.length, ⋯⟩ - List.formPerm_pow_apply_get Mathlib.GroupTheory.Perm.List
∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → ∀ (n : ℕ) (i : Fin l.length), (l.formPerm ^ n) (l.get i) = l.get ⟨(↑i + n) % l.length, ⋯⟩ - Equiv.Perm.signAux_eq_signAux2 Mathlib.GroupTheory.Perm.Sign
∀ {α : Type u} [inst : DecidableEq α] {n : ℕ} (l : List α) (f : Equiv.Perm α) (e : α ≃ Fin n), (∀ (x : α), f x ≠ x → x ∈ l) → Equiv.Perm.signAux ((e.symm.trans f).trans e) = Equiv.Perm.signAux2 l f - List.prev_get Mathlib.Data.List.Cycle
∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → ∀ (i : Fin l.length), l.prev (l.get i) ⋯ = l.get ⟨(↑i + (l.length - 1)) % l.length, ⋯⟩ - List.next_get Mathlib.Data.List.Cycle
∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → ∀ (i : Fin l.length), l.next (l.get i) ⋯ = l.get ⟨(↑i + 1) % l.length, ⋯⟩ - List.mapIdx_eq_ofFn Mathlib.Data.List.Indexes
∀ {α : Type u} {β : Type v} (l : List α) (f : ℕ → α → β), List.mapIdx f l = List.ofFn fun i => f (↑i) (l.get i) - RelSeries.fromListChain'_toFun Mathlib.Order.RelSeries
∀ {α : Type u_1} {r : Rel α α} (x : List α) (x_ne_nil : x ≠ []) (hx : List.Chain' r x) (i : Fin (x.length - 1 + 1)), (RelSeries.fromListChain' x x_ne_nil hx).toFun i = x[Fin.cast ⋯ i] - Matrix.Pivot.listTransvecCol Mathlib.LinearAlgebra.Matrix.Transvection
{𝕜 : Type u_3} → [inst : Field 𝕜] → {r : ℕ} → Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 → List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) - Matrix.Pivot.listTransvecRow Mathlib.LinearAlgebra.Matrix.Transvection
{𝕜 : Type u_3} → [inst : Field 𝕜] → {r : ℕ} → Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 → List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) - Matrix.Pivot.listTransvecCol.eq_1 Mathlib.LinearAlgebra.Matrix.Transvection
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜), Matrix.Pivot.listTransvecCol M = List.ofFn fun i => Matrix.transvection (Sum.inl i) (Sum.inr ()) (-M (Sum.inl i) (Sum.inr ()) / M (Sum.inr ()) (Sum.inr ())) - Matrix.Pivot.listTransvecRow.eq_1 Mathlib.LinearAlgebra.Matrix.Transvection
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜), Matrix.Pivot.listTransvecRow M = List.ofFn fun i => Matrix.transvection (Sum.inr ()) (Sum.inl i) (-M (Sum.inr ()) (Sum.inl i) / M (Sum.inr ()) (Sum.inr ())) - Matrix.Pivot.listTransvecCol_getElem Mathlib.LinearAlgebra.Matrix.Transvection
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) {i : ℕ} (h : i < (Matrix.Pivot.listTransvecCol M).length), (Matrix.Pivot.listTransvecCol M)[i] = Matrix.transvection (Sum.inl ⟨i, ⋯⟩) (Sum.inr ()) (-M (Sum.inl ⟨i, ⋯⟩) (Sum.inr ()) / M (Sum.inr ()) (Sum.inr ())) - Matrix.Pivot.listTransvecRow_getElem Mathlib.LinearAlgebra.Matrix.Transvection
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) {i : ℕ} (h : i < (Matrix.Pivot.listTransvecRow M).length), (Matrix.Pivot.listTransvecRow M)[i] = Matrix.transvection (Sum.inr ()) (Sum.inl ⟨i, ⋯⟩) (-M (Sum.inr ()) (Sum.inl ⟨i, ⋯⟩) / M (Sum.inr ()) (Sum.inr ())) - Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec Mathlib.LinearAlgebra.Matrix.Transvection
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜), ∃ L L', ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal - Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero Mathlib.LinearAlgebra.Matrix.Transvection
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜), M (Sum.inr ()) (Sum.inr ()) ≠ 0 → ∃ L L', ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal - Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction Mathlib.LinearAlgebra.Matrix.Transvection
∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ}, (∀ (M : Matrix (Fin r) (Fin r) 𝕜), ∃ L₀ L₀' D₀, (List.map Matrix.TransvectionStruct.toMatrix L₀).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L₀').prod = Matrix.diagonal D₀) → ∀ (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜), ∃ L L' D, (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod = Matrix.diagonal D - List.Nat.antidiagonalTuple Mathlib.Data.Fin.Tuple.NatAntidiagonal
(k : ℕ) → ℕ → List (Fin k → ℕ) - List.Nat.antidiagonalTuple.eq_2 Mathlib.Data.Fin.Tuple.NatAntidiagonal
∀ (n : ℕ), List.Nat.antidiagonalTuple 0 n.succ = [] - List.Nat.antidiagonalTuple_zero_succ Mathlib.Data.Fin.Tuple.NatAntidiagonal
∀ (n : ℕ), List.Nat.antidiagonalTuple 0 (n + 1) = [] - List.Nat.antidiagonalTuple_zero_zero Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.antidiagonalTuple 0 0 = [![]] - List.Nat.antidiagonalTuple.eq_1 Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.antidiagonalTuple 0 0 = [![]] - List.Nat.mem_antidiagonalTuple Mathlib.Data.Fin.Tuple.NatAntidiagonal
∀ {n k : ℕ} {x : Fin k → ℕ}, x ∈ List.Nat.antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n - List.Nat.antidiagonalTuple_zero_right Mathlib.Data.Fin.Tuple.NatAntidiagonal
∀ (k : ℕ), List.Nat.antidiagonalTuple k 0 = [0] - List.Nat.antidiagonalTuple_one Mathlib.Data.Fin.Tuple.NatAntidiagonal
∀ (n : ℕ), List.Nat.antidiagonalTuple 1 n = [![n]] - List.Nat.antidiagonalTuple_two Mathlib.Data.Fin.Tuple.NatAntidiagonal
∀ (n : ℕ), List.Nat.antidiagonalTuple 2 n = List.map (fun i => ![i.1, i.2]) (List.Nat.antidiagonal n) - List.Nat.antidiagonalTuple.eq_3 Mathlib.Data.Fin.Tuple.NatAntidiagonal
∀ (x k : ℕ), List.Nat.antidiagonalTuple k.succ x = (List.Nat.antidiagonal x).bind fun ni => List.map (fun x => Fin.cons ni.1 x) (List.Nat.antidiagonalTuple k ni.2) - Composition.sigmaCompositionAux.eq_1 Mathlib.Analysis.Analytic.Composition
∀ {n : ℕ} (a : Composition n) (b : Composition a.length) (i : Fin (a.gather b).length), a.sigmaCompositionAux b i = { blocks := (a.blocks.splitWrtComposition b)[↑i], blocks_pos := ⋯, blocks_sum := ⋯ } - Composition.sigma_pi_composition_eq_iff Mathlib.Analysis.Analytic.Composition
∀ {n : ℕ} (u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))), u = v ↔ (List.ofFn fun i => (u.snd i).blocks) = List.ofFn fun i => (v.snd i).blocks - HasFDerivAt.list_prod' Mathlib.Analysis.Calculus.FDeriv.Mul
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {ι : Type u_6} {𝔸 : Type u_7} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {f : ι → E → 𝔸} {f' : ι → E →L[𝕜] 𝔸} {l : List ι} {x : E}, (∀ i ∈ l, HasFDerivAt (fun x => f i x) (f' i) x) → HasFDerivAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (f' l[i]).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod) x - HasStrictFDerivAt.list_prod' Mathlib.Analysis.Calculus.FDeriv.Mul
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {ι : Type u_6} {𝔸 : Type u_7} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {f : ι → E → 𝔸} {f' : ι → E →L[𝕜] 𝔸} {l : List ι} {x : E}, (∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x) → HasStrictFDerivAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (f' l[i]).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod) x - HasFDerivWithinAt.list_prod' Mathlib.Analysis.Calculus.FDeriv.Mul
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_6} {𝔸 : Type u_7} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {f : ι → E → 𝔸} {f' : ι → E →L[𝕜] 𝔸} {l : List ι} {x : E}, (∀ i ∈ l, HasFDerivWithinAt (fun x => f i x) (f' i) s x) → HasFDerivWithinAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (f' l[i]).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod) s x - fderiv_list_prod' Mathlib.Analysis.Calculus.FDeriv.Mul
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {ι : Type u_6} {𝔸 : Type u_7} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {f : ι → E → 𝔸} {l : List ι} {x : E}, (∀ i ∈ l, DifferentiableAt 𝕜 (fun x => f i x) x) → fderiv 𝕜 (fun x => (List.map (fun x_1 => f x_1 x) l).prod) x = ∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (fderiv 𝕜 (fun x => f l[i] x) x).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod - fderivWithin_list_prod' Mathlib.Analysis.Calculus.FDeriv.Mul
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_6} {𝔸 : Type u_7} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {f : ι → E → 𝔸} {l : List ι} {x : E}, UniqueDiffWithinAt 𝕜 s x → (∀ i ∈ l, DifferentiableWithinAt 𝕜 (fun x => f i x) s x) → fderivWithin 𝕜 (fun x => (List.map (fun x_1 => f x_1 x) l).prod) s x = ∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (fderivWithin 𝕜 (fun x => f l[i] x) s x).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod - hasStrictFDerivAt_list_prod' Mathlib.Analysis.Calculus.FDeriv.Mul
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} {𝔸 : Type u_7} [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸] [inst_3 : Fintype ι] {l : List ι} {x : ι → 𝔸}, HasStrictFDerivAt (fun x => (List.map x l).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l)).prod • (ContinuousLinearMap.proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod) x - hasFDerivAt_list_prod' Mathlib.Analysis.Calculus.FDeriv.Mul
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} {𝔸' : Type u_8} [inst_1 : NormedCommRing 𝔸'] [inst_2 : NormedAlgebra 𝕜 𝔸'] [inst_3 : Fintype ι] {l : List ι} {x : ι → 𝔸'}, HasFDerivAt (fun x => (List.map x l).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l)).prod • (ContinuousLinearMap.proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod) x - hasFDerivAt_list_prod_attach' Mathlib.Analysis.Calculus.FDeriv.Mul
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} {𝔸 : Type u_7} [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸] [inst_3 : DecidableEq ι] {l : List ι} {x : { i // i ∈ l } → 𝔸}, HasFDerivAt (fun x => (List.map x l.attach).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l.attach)).prod • (ContinuousLinearMap.proj l.attach[Fin.cast ⋯ i]).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod) x - hasStrictFDerivAt_list_prod_attach' Mathlib.Analysis.Calculus.FDeriv.Mul
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} {𝔸 : Type u_7} [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸] [inst_3 : DecidableEq ι] {l : List ι} {x : { i // i ∈ l } → 𝔸}, HasStrictFDerivAt (fun x => (List.map x l.attach).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l.attach)).prod • (ContinuousLinearMap.proj l.attach[Fin.cast ⋯ i]).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod) x - YoungDiagram.rowLen_ofRowLens Mathlib.Combinatorics.Young.YoungDiagram
∀ {w : List ℕ} {hw : List.Sorted (fun x1 x2 => x1 ≥ x2) w} (i : Fin w.length), (YoungDiagram.ofRowLens w hw).rowLen ↑i = w[i] - Primrec.list_ofFn Mathlib.Computability.Primrec
∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {n : ℕ} {f : Fin n → α → σ}, (∀ (i : Fin n), Primrec (f i)) → Primrec fun a => List.ofFn fun i => f i a - Computable.list_ofFn Mathlib.Computability.Partrec
∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {n : ℕ} {f : Fin n → α → σ}, (∀ (i : Fin n), Computable (f i)) → Computable fun a => List.ofFn fun i => f i a - Turing.ToPartrec.Code.exists_code.comp Mathlib.Computability.TMToPartrec
∀ {m n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} {g : Fin n → Mathlib.Vector ℕ m →. ℕ}, (∃ c, ∀ (v : Mathlib.Vector ℕ n), c.eval ↑v = pure <$> f v) → (∀ (i : Fin n), ∃ c, ∀ (v : Mathlib.Vector ℕ m), c.eval ↑v = pure <$> g i v) → ∃ c, ∀ (v : Mathlib.Vector ℕ m), c.eval ↑v = pure <$> ((Mathlib.Vector.mOfFn fun i => g i v) >>= f) - FinEnum.toList.eq_1 Mathlib.Data.FinEnum
∀ (α : Type u_1) [inst : FinEnum α], FinEnum.toList α = List.map (⇑FinEnum.equiv.symm) (List.finRange (FinEnum.card α)) - List.get_enum Mathlib.Data.List.Enum
∀ {α : Type u_1} (l : List α) (i : Fin l.enum.length), l.enum.get i = (↑i, l.get (Fin.cast ⋯ i)) - List.get_enumFrom Mathlib.Data.List.Enum
∀ {α : Type u_1} (l : List α) (n : ℕ) (i : Fin (List.enumFrom n l).length), (List.enumFrom n l).get i = (n + ↑i, l.get (Fin.cast ⋯ i))
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from witin the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?a
If the pattern has parameters, they are matched in any order. Both of these will find
List.map
:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→
and∀
) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsum
even though the hypothesisf i < g i
is not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
woould find all lemmas which mention the constants Real.sin
and tsum
, have "two"
as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _
(if
there were any such lemmas). Metavariables (?a
) are
assigned independently in each filter.
The #lucky
button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision 7eaed1d
serving mathlib revision 329f679