Loogle!

Result

Found 3201 declarations mentioning Finsupp. Of these, 151 have a name containing "ind".

• Finsupp.single_eq_set_indicator 📋 Mathlib.Data.Finsupp.Single
  {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} : (⇑fun₀ | a => b) = {a}.indicator fun x => b
• Finsupp.induction_linear 📋 Mathlib.Algebra.Group.Finsupp
  {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0) (add : ∀ (f g : ι →₀ M), motive f → motive g → motive (f + g)) (single : ∀ (a : ι) (b : M), motive fun₀ | a => b) : motive f
• Finsupp.induction 📋 Mathlib.Algebra.Group.Finsupp
  {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0) (single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive ((fun₀ | a => b) + f)) : motive f
• Finsupp.induction₂ 📋 Mathlib.Algebra.Group.Finsupp
  {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0) (add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (f + fun₀ | a => b)) : motive f
• Finsupp.induction_on_max 📋 Mathlib.Algebra.Group.Finsupp
  {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [LinearOrder ι] {p : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : p 0) (single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p ((fun₀ | a => b) + f)) : p f
• Finsupp.induction_on_max₂ 📋 Mathlib.Algebra.Group.Finsupp
  {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [LinearOrder ι] {p : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : p 0) (add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + fun₀ | a => b)) : p f
• Finsupp.induction_on_min 📋 Mathlib.Algebra.Group.Finsupp
  {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [LinearOrder ι] {p : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : p 0) (single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p ((fun₀ | a => b) + f)) : p f
• Finsupp.induction_on_min₂ 📋 Mathlib.Algebra.Group.Finsupp
  {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [LinearOrder ι] {p : (ι →₀ M) → Prop} (f : ι →₀ M) (h0 : p 0) (ha : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (f + fun₀ | a => b)) : p f
• Finsupp.indicator 📋 Mathlib.Data.Finsupp.Indicator
  {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α) : ι →₀ α
• Finsupp.indicator_injective 📋 Mathlib.Data.Finsupp.Indicator
  {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) : Function.Injective fun f => Finsupp.indicator s f
• Finsupp.single_eq_indicator 📋 Mathlib.Data.Finsupp.Indicator
  {ι : Type u_1} {α : Type u_2} [Zero α] (i : ι) (b : α) : (fun₀ | i => b) = Finsupp.indicator {i} fun x x_1 => b
• Finsupp.indicator_of_mem 📋 Mathlib.Data.Finsupp.Indicator
  {ι : Type u_1} {α : Type u_2} [Zero α] {s : Finset ι} {i : ι} (hi : i ∈ s) (f : (i : ι) → i ∈ s → α) : (Finsupp.indicator s f) i = f i hi
• Finsupp.indicator_of_notMem 📋 Mathlib.Data.Finsupp.Indicator
  {ι : Type u_1} {α : Type u_2} [Zero α] {s : Finset ι} {i : ι} (hi : i ∉ s) (f : (i : ι) → i ∈ s → α) : (Finsupp.indicator s f) i = 0
• Finsupp.indicator_of_not_mem 📋 Mathlib.Data.Finsupp.Indicator
  {ι : Type u_1} {α : Type u_2} [Zero α] {s : Finset ι} {i : ι} (hi : i ∉ s) (f : (i : ι) → i ∈ s → α) : (Finsupp.indicator s f) i = 0
• Finsupp.indicator_apply 📋 Mathlib.Data.Finsupp.Indicator
  {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α) (i : ι) [DecidableEq ι] : (Finsupp.indicator s f) i = if hi : i ∈ s then f i hi else 0
• Finsupp.indicator.eq_1 📋 Mathlib.Data.Finsupp.Indicator
  {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α) : Finsupp.indicator s f = { support := Finset.map (Function.Embedding.subtype fun x => x ∈ s) {i | f ↑i ⋯ ≠ 0}, toFun := fun i => if H : i ∈ s then f i H else 0, mem_support_toFun := ⋯ }
• Finsupp.prod_zero_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {h : α → M → N} : Finsupp.prod 0 h = 1
• Finsupp.sum_zero_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {h : α → M → N} : Finsupp.sum 0 h = 0
• Finsupp.indicator_eq_sum_single 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} [AddCommMonoid M] (s : Finset α) (f : α → M) : (Finsupp.indicator s fun x x_1 => f x) = ∑ x ∈ s, fun₀ | x => f x
• Finsupp.prod_mapRange_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [Zero M] [Zero M'] [CommMonoid N] {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h : α → M' → N} (h0 : ∀ (a : α), h a 0 = 1) : (Finsupp.mapRange f hf g).prod h = g.prod fun a b => h a (f b)
• Finsupp.sum_mapRange_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [Zero M] [Zero M'] [AddCommMonoid N] {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h : α → M' → N} (h0 : ∀ (a : α), h a 0 = 0) : (Finsupp.mapRange f hf g).sum h = g.sum fun a b => h a (f b)
• Finsupp.prod_neg_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {G : Type u_12} [SubtractionMonoid G] [CommMonoid M] {g : α →₀ G} {h : α → G → M} (h0 : ∀ (a : α), h a 0 = 1) : (-g).prod h = g.prod fun a b => h a (-b)
• Finsupp.sum_neg_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {G : Type u_12} [SubtractionMonoid G] [AddCommMonoid M] {g : α →₀ G} {h : α → G → M} (h0 : ∀ (a : α), h a 0 = 0) : (-g).sum h = g.sum fun a b => h a (-b)
• Finsupp.indicator_eq_sum_attach_single 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} [AddCommMonoid M] {s : Finset α} (f : (a : α) → a ∈ s → M) : Finsupp.indicator s f = ∑ x ∈ s.attach, fun₀ | ↑x => f ↑x ⋯
• Finsupp.sum_sum_index' 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {ι : Type u_2} {A : Type u_4} {C : Type u_6} [AddCommMonoid A] [AddCommMonoid C] {t : ι → A → C} {s : Finset α} {f : α → ι →₀ A} (h0 : ∀ (i : ι), t i 0 = 0) (h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y) : (∑ x ∈ s, f x).sum t = ∑ x ∈ s, (f x).sum t
• Finsupp.prod_finset_sum_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [AddCommMonoid M] [CommMonoid N] {s : Finset ι} {g : ι → α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), h a 0 = 1) (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) : ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
• Finsupp.sum_finset_sum_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [AddCommMonoid M] [AddCommMonoid N] {s : Finset ι} {g : ι → α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), h a 0 = 0) (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) : ∑ i ∈ s, (g i).sum h = (∑ i ∈ s, g i).sum h
• Finsupp.prod_sum_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [AddCommMonoid N] [CommMonoid P] {f : α →₀ M} {g : α → M → β →₀ N} {h : β → N → P} (h_zero : ∀ (a : β), h a 0 = 1) (h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ * h a b₂) : (f.sum g).prod h = f.prod fun a b => (g a b).prod h
• Finsupp.sum_sum_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [AddCommMonoid N] [AddCommMonoid P] {f : α →₀ M} {g : α → M → β →₀ N} {h : β → N → P} (h_zero : ∀ (a : β), h a 0 = 0) (h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂) : (f.sum g).sum h = f.sum fun a b => (g a b).sum h
• Finsupp.multiset_sum_sum_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddCommMonoid M] [AddCommMonoid N] (f : Multiset (α →₀ M)) (h : α → M → N) (h₀ : ∀ (a : α), h a 0 = 0) (h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) : f.sum.sum h = (Multiset.map (fun g => g.sum h) f).sum
• Finsupp.prod_add_index' 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), h a 0 = 1) (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) : (f + g).prod h = f.prod h * g.prod h
• Finsupp.sum_add_index' 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), h a 0 = 0) (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) : (f + g).sum h = f.sum h + g.sum h
• Finsupp.prod_add_index_of_disjoint 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} [AddCommMonoid M] {f1 f2 : α →₀ M} (hd : Disjoint f1.support f2.support) {β : Type u_16} [CommMonoid β] (g : α → M → β) : (f1 + f2).prod g = f1.prod g * f2.prod g
• Finsupp.sum_add_index_of_disjoint 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} [AddCommMonoid M] {f1 f2 : α →₀ M} (hd : Disjoint f1.support f2.support) {β : Type u_16} [AddCommMonoid β] (g : α → M → β) : (f1 + f2).sum g = f1.sum g + f2.sum g
• Finsupp.sum_sub_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {γ : Type u_3} {β : Type u_7} [AddGroup β] [AddCommGroup γ] {f g : α →₀ β} {h : α → β → γ} (h_sub : ∀ (a : α) (b₁ b₂ : β), h a (b₁ - b₂) = h a b₁ - h a b₂) : (f - g).sum h = f.sum h - g.sum h
• Finsupp.sum_hom_add_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] {f g : α →₀ M} (h : α → M →+ N) : ((f + g).sum fun x => ⇑(h x)) = (f.sum fun x => ⇑(h x)) + g.sum fun x => ⇑(h x)
• Finsupp.prod_add_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {N : Type u_10} [DecidableEq α] [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1) (h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) : (f + g).prod h = f.prod h * g.prod h
• Finsupp.sum_add_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {N : Type u_10} [DecidableEq α] [AddZeroClass M] [AddCommMonoid N] {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0) (h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) : (f + g).sum h = f.sum h + g.sum h
• Finsupp.prod_hom_add_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} (h : α → Multiplicative M →* N) : ((f + g).prod fun a b => (h a) (Multiplicative.ofAdd b)) = (f.prod fun a b => (h a) (Multiplicative.ofAdd b)) * g.prod fun a b => (h a) (Multiplicative.ofAdd b)
• Finsupp.filter_eq_indicator 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {M : Type u_5} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) : ⇑(Finsupp.filter p f) = {x | p x}.indicator ⇑f
• Finsupp.prod_subtypeDomain_index 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] {p : α → Prop} [CommMonoid N] {v : α →₀ M} {h : α → M → N} (hp : ∀ x ∈ v.support, p x) : ((Finsupp.subtypeDomain p v).prod fun a b => h (↑a) b) = v.prod h
• Finsupp.sum_subtypeDomain_index 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] {p : α → Prop} [AddCommMonoid N] {v : α →₀ M} {h : α → M → N} (hp : ∀ x ∈ v.support, p x) : ((Finsupp.subtypeDomain p v).sum fun a b => h (↑a) b) = v.sum h
• Finsupp.prod_filter_index 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) [CommMonoid N] (g : α → M → N) : (Finsupp.filter p f).prod g = ∏ x ∈ (Finsupp.filter p f).support, g x (f x)
• Finsupp.sum_filter_index 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) [AddCommMonoid N] (g : α → M → N) : (Finsupp.filter p f).sum g = ∑ x ∈ (Finsupp.filter p f).support, g x (f x)
• Finsupp.prod_mapDomain_index_inj 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [CommMonoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (hf : Function.Injective f) : (Finsupp.mapDomain f s).prod h = s.prod fun a b => h (f a) b
• Finsupp.sum_mapDomain_index_inj 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (hf : Function.Injective f) : (Finsupp.mapDomain f s).sum h = s.sum fun a b => h (f a) b
• Finsupp.sum_curry_index 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [DecidableEq α] [Zero M] [AddCommMonoid N] (f : α × β →₀ M) (g : α → β → M → N) : (f.curry.sum fun a f => f.sum (g a)) = f.sum fun p c => g p.1 p.2 c
• Finsupp.sum_uncurry_index 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [AddCommMonoid N] (f : α →₀ β →₀ M) (g : α × β → M → N) : (f.uncurry.sum fun p c => g p c) = f.sum fun a f => f.sum fun b => g (a, b)
• Finsupp.sum_uncurry_index' 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [AddCommMonoid N] (f : α →₀ β →₀ M) (g : α → β → M → N) : (f.uncurry.sum fun p c => g p.1 p.2 c) = f.sum fun a f => f.sum (g a)
• Finsupp.prod_mapDomain_index 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [CommMonoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (h_zero : ∀ (b : β), h b 0 = 1) (h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ * h b m₂) : (Finsupp.mapDomain f s).prod h = s.prod fun a m => h (f a) m
• Finsupp.sum_mapDomain_index 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (h_zero : ∀ (b : β), h b 0 = 0) (h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ + h b m₂) : (Finsupp.mapDomain f s).sum h = s.sum fun a m => h (f a) m
• Finsupp.sum_mapDomain_index_addMonoidHom 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] {f : α → β} {s : α →₀ M} (h : β → M →+ N) : ((Finsupp.mapDomain f s).sum fun b m => (h b) m) = s.sum fun a m => (h (f a)) m
• Finsupp.sum_smul_index' 📋 Mathlib.Data.Finsupp.SMul
  {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_6} [Zero M] [SMulZeroClass R M] [AddCommMonoid N] {g : α →₀ M} {b : R} {h : α → M → N} (h0 : ∀ (i : α), h i 0 = 0) : (b • g).sum h = g.sum fun i c => h i (b • c)
• Finsupp.sum_smul_index 📋 Mathlib.Data.Finsupp.SMul
  {α : Type u_1} {M : Type u_3} {R : Type u_6} [MulZeroClass R] [AddCommMonoid M] {g : α →₀ R} {b : R} {h : α → R → M} (h0 : ∀ (i : α), h i 0 = 0) : (b • g).sum h = g.sum fun i a => h i (b * a)
• Finsupp.sum_smul_index_addMonoidHom 📋 Mathlib.Data.Finsupp.SMul
  {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_6} [AddZeroClass M] [AddCommMonoid N] [SMulZeroClass R M] {g : α →₀ M} {b : R} {h : α → M →+ N} : ((b • g).sum fun a => ⇑(h a)) = g.sum fun i c => (h i) (b • c)
• Finsupp.sum_smul_index_linearMap' 📋 Mathlib.LinearAlgebra.Finsupp.LSum
  {α : Type u_1} {R : Type u_3} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {v : α →₀ M} {c : R} {h : α → M →ₗ[R] M₂} : ((c • v).sum fun a => ⇑(h a)) = c • v.sum fun a => ⇑(h a)
• Finsupp.sum_smul_index_semilinearMap' 📋 Mathlib.LinearAlgebra.Finsupp.LSum
  {α : Type u_1} {R : Type u_3} {R₂ : Type u_4} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R₂ M₂] {σ : R →+* R₂} {v : α →₀ M} {c : R} {h : α → M →ₛₗ[σ] M₂} : ((c • v).sum fun a => ⇑(h a)) = σ c • v.sum fun a => ⇑(h a)
• Finsupp.prod_option_index 📋 Mathlib.Data.Finsupp.Option
  {α : Type u_1} {M : Type u_2} {N : Type u_3} [AddZeroClass M] [CommMonoid N] (f : Option α →₀ M) (b : Option α → M → N) (h_zero : ∀ (o : Option α), b o 0 = 1) (h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂) : f.prod b = b none (f none) * f.some.prod fun a => b (some a)
• Finsupp.sum_option_index 📋 Mathlib.Data.Finsupp.Option
  {α : Type u_1} {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddCommMonoid N] (f : Option α →₀ M) (b : Option α → M → N) (h_zero : ∀ (o : Option α), b o 0 = 0) (h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ + b o m₂) : f.sum b = b none (f none) + f.some.sum fun a => b (some a)
• Finsupp.sum_option_index_smul 📋 Mathlib.Data.Finsupp.Option
  {α : Type u_1} {M : Type u_2} {R : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (f : Option α →₀ R) (b : Option α → M) : (f.sum fun o r => r • b o) = f none • b none + f.some.sum fun a r => r • b (some a)
• Finsupp.linearCombination_single_index 📋 Mathlib.LinearAlgebra.Finsupp.LinearCombination
  (α : Type u_1) (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (c : M) (a : α) (f : α →₀ R) [DecidableEq α] : (Finsupp.linearCombination R (Pi.single a c)) f = f a • c
• Module.Basis.reindex.eq_1 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (e : ι ≃ ι') : b.reindex e = { repr := b.repr ≪≫ₗ Finsupp.domLCongr e }
• Module.Basis.repr_reindex 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (x : M) (e : ι ≃ ι') : (b.reindex e).repr x = Finsupp.mapDomain (⇑e) (b.repr x)
• Module.Basis.repr_reindex_apply 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (x : M) (e : ι ≃ ι') (i' : ι') : ((b.reindex e).repr x) i' = (b.repr x) (e.symm i')
• Module.Basis.reindexRange_repr_self 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (i : ι) : b.reindexRange.repr (b i) = fun₀ | ⟨b i, ⋯⟩ => 1
• Module.Basis.reindexFinsetRange_repr_self 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) [Fintype ι] [DecidableEq M] (i : ι) : b.reindexFinsetRange.repr (b i) = fun₀ | ⟨b i, ⋯⟩ => 1
• Module.Basis.reindexRange_repr' 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (x : M) {bi : M} {i : ι} (h : b i = bi) : (b.reindexRange.repr x) ⟨bi, ⋯⟩ = (b.repr x) i
• Module.Basis.reindexRange_repr 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (x : M) (i : ι) (h : b i ∈ Set.range ⇑b := ⋯) : (b.reindexRange.repr x) ⟨b i, h⟩ = (b.repr x) i
• Module.Basis.reindexFinsetRange_repr 📋 Mathlib.LinearAlgebra.Basis.Defs
  {ι : Type u_10} {R : Type u_11} {M : Type u_12} [Semiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) [Fintype ι] [DecidableEq M] (x : M) (i : ι) (h : b i ∈ Finset.image (⇑b) Finset.univ := ⋯) : (b.reindexFinsetRange.repr x) ⟨b i, h⟩ = (b.repr x) i
• LinearIndependent.repr 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : ↥(Submodule.span R (Set.range v)) →ₗ[R] ι →₀ R
• LinearIndependent.linearCombinationEquiv 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : (ι →₀ R) ≃ₗ[R] ↥(Submodule.span R (Set.range v))
• LinearIndependent.repr.congr_simp 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : hv.repr = hv.repr
• LinearIndependent.linearCombinationEquiv.congr_simp 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : hv.linearCombinationEquiv = hv.linearCombinationEquiv
• LinearIndependent.finsuppLinearCombination_injective 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v → Function.Injective ⇑(Finsupp.linearCombination R v)
• LinearIndependent.linearCombination_injective 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v → Function.Injective ⇑(Finsupp.linearCombination R v)
• linearIndependent_iff_injective_finsuppLinearCombination 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v ↔ Function.Injective ⇑(Finsupp.linearCombination R v)
• linearIndependent_iff_injective_linearCombination 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v ↔ Function.Injective ⇑(Finsupp.linearCombination R v)
• LinearIndependent.eq_1 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} (R : Type u_2) {M : Type u_4} (v : ι → M) [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v = Function.Injective ⇑(Finsupp.linearCombination R v)
• LinearIndependent.linearCombination_comp_repr 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : Finsupp.linearCombination R v ∘ₗ hv.repr = (Submodule.span R (Set.range v)).subtype
• linearIndependent_iff 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndependent R v ↔ ∀ (l : ι →₀ R), (Finsupp.linearCombination R v) l = 0 → l = 0
• linearIndependent_iffₛ 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndependent R v ↔ ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
• LinearIndependent.repr.eq_1 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : hv.repr = ↑hv.linearCombinationEquiv.symm
• LinearIndependent.span_repr_eq 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) [Nontrivial R] (x : ↥(Submodule.span R (Set.range v))) : Span.repr R (Set.range v) x = Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)
• LinearIndependent.repr_eq_single 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) (i : ι) (x : ↥(Submodule.span R (Set.range v))) (hx : ↑x = v i) : hv.repr x = fun₀ | i => 1
• linearIndependent_iff_ker 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndependent R v ↔ LinearMap.ker (Finsupp.linearCombination R v) = ⊥
• LinearIndependent.linearCombination_repr 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) (x : ↥(Submodule.span R (Set.range v))) : (Finsupp.linearCombination R v) (hv.repr x) = ↑x
• linearIndepOn_iff 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndepOn R v s ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0
• LinearIndependent.repr_eq 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) {l : ι →₀ R} {x : ↥(Submodule.span R (Set.range v))} (eq : (Finsupp.linearCombination R v) l = ↑x) : hv.repr x = l
• LinearIndependent.repr_range 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : LinearMap.range hv.repr = ⊤
• linearIndepOn_iff_disjoint 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndepOn R v s ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))
• LinearIndependent.linearCombinationEquiv_apply_coe 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) (a✝ : ι →₀ R) : ↑(hv.linearCombinationEquiv a✝) = (Finsupp.linearCombination R v) a✝
• LinearIndependent.repr_ker 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) : LinearMap.ker hv.repr = ⊥
• linearIndepOn_iffₛ 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndepOn R v s ↔ ∀ f ∈ Finsupp.supported R R s, ∀ g ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g
• linearIndependent_comp_subtypeₛ 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndepOn R v s ↔ ∀ f ∈ Finsupp.supported R R s, ∀ g ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g
• linearIndependent_subtypeₛ 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndepOn R v s ↔ ∀ f ∈ Finsupp.supported R R s, ∀ g ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g
• linearIndepOn_iff_linearCombinationOnₛ 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndepOn R v s ↔ Function.Injective ⇑(Finsupp.linearCombinationOn ι M R v s)
• linearIndependent_iff_linearCombinationOnₛ 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] : LinearIndepOn R v s ↔ Function.Injective ⇑(Finsupp.linearCombinationOn ι M R v s)
• linearIndepOn_iff_linearCombinationOn 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] : LinearIndepOn R v s ↔ LinearMap.ker (Finsupp.linearCombinationOn ι M R v s) = ⊥
• LinearIndependent.linearCombinationEquiv_symm_apply 📋 Mathlib.LinearAlgebra.LinearIndependent.Defs
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) (a✝ : ↥(Submodule.span R (Set.range v))) : hv.linearCombinationEquiv.symm a✝ = ((LinearEquiv.ofInjective (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.linearCombination R v) ⋯) ⋯).toEquiv.trans (LinearEquiv.ofTop (LinearMap.range (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.linearCombination R v) ⋯)) ⋯).toEquiv).invFun a✝
• LinearIndependent.linearCombination_ne_of_notMem_support 📋 Mathlib.LinearAlgebra.LinearIndependent.Basic
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] (hv : LinearIndependent R v) {x : ι} (f : ι →₀ R) (h : x ∉ f.support) : (Finsupp.linearCombination R v) f ≠ v x
• LinearIndependent.linearCombination_ne_of_not_mem_support 📋 Mathlib.LinearAlgebra.LinearIndependent.Basic
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] (hv : LinearIndependent R v) {x : ι} (f : ι →₀ R) (h : x ∉ f.support) : (Finsupp.linearCombination R v) f ≠ v x
• Finsupp.linearIndependent_single_one 📋 Mathlib.LinearAlgebra.Finsupp.VectorSpace
  (R : Type u_1) (ι : Type u_3) [Semiring R] : LinearIndependent R fun i => fun₀ | i => 1
• Finsupp.linearIndependent_single 📋 Mathlib.LinearAlgebra.Finsupp.VectorSpace
  {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {φ : ι → Type u_4} (f : (i : ι) → φ i → M) (hf : ∀ (i : ι), LinearIndependent R (f i)) : LinearIndependent R fun ix => fun₀ | ix.fst => f ix.fst ix.snd
• Finsupp.linearIndependent_single_iff 📋 Mathlib.LinearAlgebra.Finsupp.VectorSpace
  {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {φ : ι → Type u_4} {f : (i : ι) → φ i → M} : (LinearIndependent R fun ix => fun₀ | ix.fst => f ix.fst ix.snd) ↔ ∀ (i : ι), LinearIndependent R (f i)
• Finsupp.linearIndependent_single_of_ne_zero 📋 Mathlib.LinearAlgebra.Finsupp.VectorSpace
  {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : ι → M} (hv : ∀ (i : ι), v i ≠ 0) : LinearIndependent R fun i => fun₀ | i => v i
• union_support_maximal_linearIndependent_eq_range_basis 📋 Mathlib.LinearAlgebra.Basis.Cardinality
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Nontrivial R] [Module R M] {ι : Type w} (b : Module.Basis ι R M) {κ : Type w'} (v : κ → M) (ind : LinearIndependent R v) (m : ind.Maximal) : ⋃ k, ↑(b.repr (v k)).support = Set.univ
• Finsupp.sum_le_sum_index 📋 Mathlib.Data.Finsupp.Order
  {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] [DecidableEq ι] {f₁ f₂ : ι →₀ α} {h : ι → α → β} (hf : f₁ ≤ f₂) (hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)) (hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0) : f₁.sum h ≤ f₂.sum h
• MvPolynomial.induction_on' 📋 Mathlib.Algebra.MvPolynomial.Basic
  {R : Type u} {σ : Type u_1} [CommSemiring R] {P : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (monomial : ∀ (u : σ →₀ ℕ) (a : R), P ((MvPolynomial.monomial u) a)) (add : ∀ (p q : MvPolynomial σ R), P p → P q → P (p + q)) : P p
• MvPolynomial.induction_on_monomial 📋 Mathlib.Algebra.MvPolynomial.Basic
  {R : Type u} {σ : Type u_1} [CommSemiring R] {motive : MvPolynomial σ R → Prop} (C : ∀ (a : R), motive (MvPolynomial.C a)) (mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * MvPolynomial.X n)) (s : σ →₀ ℕ) (a : R) : motive ((MvPolynomial.monomial s) a)
• MvPolynomial.induction_on''' 📋 Mathlib.Algebra.MvPolynomial.Basic
  {R : Type u} {σ : Type u_1} [CommSemiring R] {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (C : ∀ (a : R), motive (MvPolynomial.C a)) (monomial_add : ∀ (a : σ →₀ ℕ) (b : R) (f : MvPolynomial σ R), a ∉ f.support → b ≠ 0 → motive f → motive ((MvPolynomial.monomial a) b + f)) : motive p
• MvPolynomial.monomial_add_induction_on 📋 Mathlib.Algebra.MvPolynomial.Basic
  {R : Type u} {σ : Type u_1} [CommSemiring R] {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (C : ∀ (a : R), motive (MvPolynomial.C a)) (monomial_add : ∀ (a : σ →₀ ℕ) (b : R) (f : MvPolynomial σ R), a ∉ f.support → b ≠ 0 → motive f → motive ((MvPolynomial.monomial a) b + f)) : motive p
• MvPolynomial.monomial_sum_index 📋 Mathlib.Algebra.MvPolynomial.Basic
  {R : Type u} {σ : Type u_1} [CommSemiring R] {α : Type u_2} (s : Finset α) (f : α → σ →₀ ℕ) (a : R) : (MvPolynomial.monomial (∑ i ∈ s, f i)) a = MvPolynomial.C a * ∏ i ∈ s, (MvPolynomial.monomial (f i)) 1
• MvPolynomial.monomial_finsupp_sum_index 📋 Mathlib.Algebra.MvPolynomial.Basic
  {R : Type u} {σ : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [Zero β] (f : α →₀ β) (g : α → β → σ →₀ ℕ) (a : R) : (MvPolynomial.monomial (f.sum g)) a = MvPolynomial.C a * f.prod fun a b => (MvPolynomial.monomial (g a b)) 1
• MvPolynomial.induction_on'' 📋 Mathlib.Algebra.MvPolynomial.Basic
  {R : Type u} {σ : Type u_1} [CommSemiring R] {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (C : ∀ (a : R), motive (MvPolynomial.C a)) (monomial_add : ∀ (a : σ →₀ ℕ) (b : R) (f : MvPolynomial σ R), a ∉ f.support → b ≠ 0 → motive f → motive ((MvPolynomial.monomial a) b) → motive ((MvPolynomial.monomial a) b + f)) (mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * MvPolynomial.X n)) : motive p
• Nat.factorization_eq_zero_of_remainder 📋 Mathlib.Data.Nat.Factorization.Defs
  {p r : ℕ} (i : ℕ) (hr : ¬p ∣ r) : (p * i + r).factorization p = 0
• Nat.factorization_eq_zero_iff_remainder 📋 Mathlib.Data.Nat.Factorization.Basic
  {p r : ℕ} (i : ℕ) (pp : Nat.Prime p) (hr0 : r ≠ 0) : ¬p ∣ r ↔ (p * i + r).factorization p = 0
• basisOfLinearIndependentOfCardEqFinrank_repr_apply 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [Nonempty ι] [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = Module.finrank K V) (a✝ : V) : (basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr a✝ = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range b)) LinearMap.id ⋯) a✝)
• setBasisOfLinearIndependentOfCardEqFinrank_repr_apply 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Nonempty ↑s] [Fintype ↑s] (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.toFinset.card = Module.finrank K V) (a✝ : V) : (setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr a✝ = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a✝)
• finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply 📋 Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (hs : s.Nonempty) (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.card = Module.finrank K V) (a✝ : V) : (finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq).repr a✝ = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a✝)
• MvPolynomial.bind₂_monomial_one 📋 Mathlib.Algebra.MvPolynomial.Monad
  {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial σ S) (d : σ →₀ ℕ) : (MvPolynomial.bind₂ f) ((MvPolynomial.monomial d) 1) = (MvPolynomial.monomial d) 1
• MvPolynomial.bind₁_monomial 📋 Mathlib.Algebra.MvPolynomial.Monad
  {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → MvPolynomial τ R) (d : σ →₀ ℕ) (r : R) : (MvPolynomial.bind₁ f) ((MvPolynomial.monomial d) r) = MvPolynomial.C r * ∏ i ∈ d.support, f i ^ d i
• MvPolynomial.bind₂_monomial 📋 Mathlib.Algebra.MvPolynomial.Monad
  {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial σ S) (d : σ →₀ ℕ) (r : R) : (MvPolynomial.bind₂ f) ((MvPolynomial.monomial d) r) = f r * (MvPolynomial.monomial d) 1
• Finsupp.weight_single_index 📋 Mathlib.Data.Finsupp.Weight
  {σ : Type u_1} {M : Type u_2} {R : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [DecidableEq σ] (s : σ) (c : M) (f : σ →₀ R) : (Finsupp.weight (Pi.single s c)) f = f s • c
• Submodule.LinearDisjoint.linearIndependent_left_of_flat 📋 Mathlib.LinearAlgebra.LinearDisjoint
  {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M N : Submodule R S} (H : M.LinearDisjoint N) [Module.Flat R ↥N] {ι : Type u_1} {m : ι → ↥M} (hm : LinearIndependent R m) : LinearMap.ker (Submodule.mulLeftMap N m) = ⊥
• Submodule.LinearDisjoint.linearIndependent_right_of_flat 📋 Mathlib.LinearAlgebra.LinearDisjoint
  {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {M N : Submodule R S} (H : M.LinearDisjoint N) [Module.Flat R ↥M] {ι : Type u_1} {n : ι → ↥N} (hn : LinearIndependent R n) : LinearMap.ker (M.mulRightMap n) = ⊥
• Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent 📋 Mathlib.RingTheory.LinearDisjoint
  {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (A B : Subalgebra R S) {ι : Type u_1} (b : ι → ↥B) : LinearMap.ker ((Subalgebra.toSubmodule A).mulRightMap b) = ⊥ ↔ LinearIndependent (↥A) (⇑B.val ∘ b)
• Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op 📋 Mathlib.RingTheory.LinearDisjoint
  {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (A B : Subalgebra R S) {ι : Type u_1} (a : ι → ↥A) : LinearMap.ker (Submodule.mulLeftMap (Subalgebra.toSubmodule B) a) = ⊥ ↔ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)
• Rep.coindFunctorIso_inv_app_hom_hom_apply_coe 📋 Mathlib.RepresentationTheory.Coinduced
  {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (X : Rep k G) (a : (Action.res (ModuleCat k) φ).obj (Rep.leftRegular k H) ⟶ X) (h : H) : ↑((ModuleCat.Hom.hom ((Rep.coindFunctorIso φ).inv.app X).hom) a) h = (CategoryTheory.ConcreteCategory.hom a.hom) fun₀ | h => 1
• Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply 📋 Mathlib.RepresentationTheory.Coinduced
  {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (X : Rep k G) (f : ↥(Representation.coindV φ X.ρ)) (d : H →₀ k) : (ModuleCat.Hom.hom ((ModuleCat.Hom.hom ((Rep.coindFunctorIso φ).hom.app X).hom) f).hom) d = d.sum fun i c => c • ↑f i
• Rep.coindVEquiv_apply_hom 📋 Mathlib.RepresentationTheory.Coinduced
  {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) (f : ↥(Representation.coindV φ A.ρ)) : ((Rep.coindVEquiv φ A) f).hom = ModuleCat.ofHom (Finsupp.linearCombination k ↑f)
• Representation.ind 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) : Representation k H (Representation.IndV φ ρ)
• Representation.IndV.mk 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) (h : H) : A →ₗ[k] Representation.IndV φ ρ
• Representation.IndV.hom_ext 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} {B : Type u_5} [AddCommGroup A] [Module k A] (ρ : Representation k G A) [AddCommGroup B] [Module k B] {f g : Representation.IndV φ ρ →ₗ[k] B} (hfg : ∀ (h : H), f ∘ₗ Representation.IndV.mk φ ρ h = g ∘ₗ Representation.IndV.mk φ ρ h) : f = g
• Representation.IndV.hom_ext_iff 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] {φ : G →* H} {A : Type u_4} {B : Type u_5} [AddCommGroup A] [Module k A] {ρ : Representation k G A} [AddCommGroup B] [Module k B] {f g : Representation.IndV φ ρ →ₗ[k] B} : f = g ↔ ∀ (h : H), f ∘ₗ Representation.IndV.mk φ ρ h = g ∘ₗ Representation.IndV.mk φ ρ h
• Rep.indMap_hom 📋 Mathlib.RepresentationTheory.Induced
  {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) {A B : Rep k G} (f : A ⟶ B) : (Rep.indMap φ f).hom = ModuleCat.ofHom (Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ) (LinearMap.lTensor (H →₀ k) (ModuleCat.Hom.hom f.hom)) ⋯)
• Rep.indResHomEquiv_symm_apply_hom 📋 Mathlib.RepresentationTheory.Induced
  {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) (f : A ⟶ (Action.res (ModuleCat k) φ).obj B) : ((Rep.indResHomEquiv φ A B).symm f).hom = ModuleCat.ofHom (Representation.Coinvariants.lift (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) (TensorProduct.lift ((Finsupp.lift (↑A.V →ₗ[k] ↑B.1) k H) fun h => B.ρ h⁻¹ ∘ₗ ModuleCat.Hom.hom f.hom)) ⋯)
• Rep.indResAdjunction_counit_app_hom_hom 📋 Mathlib.RepresentationTheory.Induced
  (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (Y : Rep k H) : ModuleCat.Hom.hom ((Rep.indResAdjunction k φ).counit.app Y).hom = Representation.Coinvariants.lift (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) (MonoidHom.comp Y.ρ φ)) (TensorProduct.lift ((Finsupp.lift (↑Y.V →ₗ[k] ↑Y.1) k H) fun h => Y.ρ h⁻¹)) ⋯
• Rep.coinvariantsTensorIndHom_mk_tmul_indVMk 📋 Mathlib.RepresentationTheory.Induced
  {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Rep k G} {B : Rep k H} (h : H) (x : ↑A.V) (y : ↑B.V) : (CategoryTheory.ConcreteCategory.hom (Rep.coinvariantsTensorIndHom φ A B)) ((((Rep.ind φ A).coinvariantsTensorMk B) ((Representation.IndV.mk φ A.ρ h) x)) y) = ((A.coinvariantsTensorMk ((Action.res (ModuleCat k) φ).obj B)) x) ((B.ρ h) y)
• Rep.coinvariantsTensorIndInv_mk_tmul_indMk 📋 Mathlib.RepresentationTheory.Induced
  {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Rep k G} {B : Rep k H} (x : ↑A.V) (y : ↑B.V) : (CategoryTheory.ConcreteCategory.hom (Rep.coinvariantsTensorIndInv φ A B)) ((Representation.Coinvariants.mk (A.ρ.tprod (Rep.ρ ((Action.res (ModuleCat k) φ).obj B)))) (x ⊗ₜ[k] y)) = (((Rep.ind φ A).coinvariantsTensorMk B) ((Representation.IndV.mk φ A.ρ 1) x)) y
• Representation.ind_mk 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) (h₁ h₂ : H) (a : A) : ((Representation.ind φ ρ) h₁) ((Representation.IndV.mk φ ρ h₂) a) = (Representation.IndV.mk φ ρ (h₂ * h₁⁻¹)) a
• Representation.ind_apply 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) (h : H) : (Representation.ind φ ρ) h = Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) ρ) (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) ρ) (LinearMap.rTensor A (Finsupp.lmapDomain k k fun x => x * h⁻¹)) ⋯
• Rep.coinvariantsTensorIndHom.eq_1 📋 Mathlib.RepresentationTheory.Induced
  {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) : Rep.coinvariantsTensorIndHom φ A B = ModuleCat.ofHom (Representation.Coinvariants.lift (((CategoryTheory.MonoidalCategory.curriedTensor (Rep k H)).obj (Rep.ind φ A)).obj B).ρ (TensorProduct.lift (Representation.Coinvariants.lift (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) (TensorProduct.lift ((Finsupp.lift (↑A.V →ₗ[k] ↑(((Action.functorCategoryEquivalence (ModuleCat k) H).symm.inverse.obj B).obj PUnit.unit) →ₗ[k] (((CategoryTheory.MonoidalCategory.curriedTensor (Rep k G)).obj A).obj ((Action.res (ModuleCat k) φ).obj B)).ρ.Coinvariants) k H) fun g => (A.coinvariantsTensorMk ((Action.res (ModuleCat k) φ).obj B)).compl₂ (B.ρ g))) ⋯)) ⋯)
• Rep.coindToInd 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} (A : Rep k ↥S) [S.FiniteIndex] : ↑(Rep.coind S.subtype A).V →ₗ[k] ↑(Rep.ind S.subtype A).V
• Rep.indToCoind 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) : ↑(Rep.ind S.subtype A).V →ₗ[k] ↑(Rep.coind S.subtype A).V
• Rep.coindToInd.congr_simp 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} (A : Rep k ↥S) [S.FiniteIndex] : A.coindToInd = A.coindToInd
• Rep.indCoindIso_hom_hom_hom 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) [S.FiniteIndex] : ModuleCat.Hom.hom A.indCoindIso.hom.hom = A.indToCoind
• Rep.indCoindIso_inv_hom_hom 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) [S.FiniteIndex] : ModuleCat.Hom.hom A.indCoindIso.inv.hom = A.coindToInd
• Rep.coindToInd_of_support_subset_orbit 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} {A : Rep k ↥S} [S.FiniteIndex] (g : G) (f : ↑(Rep.coind S.subtype A).V) (hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g) : A.coindToInd f = (Representation.IndV.mk S.subtype A.ρ g) (↑f g)
• Rep.coindToInd_apply 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} (A : Rep k ↥S) [S.FiniteIndex] (f : ↑(Rep.coind S.subtype A).V) : A.coindToInd f = ∑ g, g.liftOn (fun g => (Representation.IndV.mk S.subtype A.ρ g) (↑f g)) ⋯
• groupHomology.H1_induction_on 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
  {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {C : ↑(groupHomology.H1 A) → Prop} (x : ↑(groupHomology.H1 A)) (h : ∀ (x : ↥(groupHomology.cycles₁ A)), C ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A)) x)) : C x
• groupHomology.H2_induction_on 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
  {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {C : ↑(groupHomology.H2 A) → Prop} (x : ↑(groupHomology.H2 A)) (h : ∀ (x : ↥(groupHomology.cycles₂ A)), C ((CategoryTheory.ConcreteCategory.hom (groupHomology.H2π A)) x)) : C x

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, 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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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 find tsum_lt_tsum even though the hypothesis f 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, _ * _, _ ^ _, |- _ < _ → _
would 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 ad0d2bb serving mathlib revision 0852c3e