Loogle!

Result

Found 35 declarations mentioning Equiv, Eq and Finset.sum.

• Equiv.sum_comp 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι ≃ κ) (g : κ → α) : ∑ i, g (e i) = ∑ i, g i
• Fintype.sum_equiv 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι ≃ κ) (f : ι → α) (g : κ → α) (h : ∀ (x : ι), f x = g (e x)) : ∑ x, f x = ∑ x, g x
• ofAdd_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] (s : Finset ι) (f : ι → α) : Multiplicative.ofAdd (∑ i ∈ s, f i) = ∏ i ∈ s, Multiplicative.ofAdd (f i)
• ofMul_prod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {ι : Type u_1} {α : Type u_3} [CommMonoid α] (s : Finset ι) (f : ι → α) : Additive.ofMul (∏ i ∈ s, f i) = ∑ i ∈ s, Additive.ofMul (f i)
• toAdd_prod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] (s : Finset ι) (f : ι → Multiplicative α) : Multiplicative.toAdd (∏ i ∈ s, f i) = ∑ i ∈ s, Multiplicative.toAdd (f i)
• toMul_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {ι : Type u_1} {α : Type u_3} [CommMonoid α] (s : Finset ι) (f : ι → Additive α) : Additive.toMul (∑ i ∈ s, f i) = ∏ i ∈ s, Additive.toMul (f i)
• Equiv.Perm.sum_comp' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (σ : Equiv.Perm α) (s : Finset α) (f : α → α → β) (hs : {a | σ a ≠ a} ⊆ ↑s) : ∑ x ∈ s, f (σ x) x = ∑ x ∈ s, f x ((Equiv.symm σ) x)
• Finset.sum_equiv 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (e : ι ≃ κ) (hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : ∑ i ∈ s, f i = ∑ i ∈ t, g i
• Finsupp.equivFunOnFinite_symm_eq_sum 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} [Fintype α] [AddCommMonoid M] (f : α → M) : Finsupp.equivFunOnFinite.symm f = ∑ a, fun₀ | a => f a
• finSigmaFinEquiv.eq_1 📋 Mathlib.Algebra.BigOperators.Fin
  (n_2 : Fin 0 → ℕ) : finSigmaFinEquiv = Equiv.equivOfIsEmpty ((i : Fin 0) × Fin (n_2 i)) (Fin (∑ i, n_2 i))
• finFunctionFinEquiv_apply 📋 Mathlib.Algebra.BigOperators.Fin
  {m n : ℕ} (f : Fin n → Fin m) : ↑(finFunctionFinEquiv f) = ∑ i, ↑(f i) * m ^ ↑i
• finFunctionFinEquiv_apply_val 📋 Mathlib.Algebra.BigOperators.Fin
  {m n : ℕ} (f : Fin n → Fin m) : ↑(finFunctionFinEquiv f) = ∑ i, ↑(f i) * m ^ ↑i
• finPiFinEquiv_apply 📋 Mathlib.Algebra.BigOperators.Fin
  {m : ℕ} {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)) : ↑(finPiFinEquiv f) = ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j)
• finSigmaFinEquiv_apply 📋 Mathlib.Algebra.BigOperators.Fin
  {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)) : ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
• finSigmaFinEquiv_one 📋 Mathlib.Algebra.BigOperators.Fin
  {n : Fin 1 → ℕ} (ij : (i : Fin 1) × Fin (n i)) : ↑(finSigmaFinEquiv ij) = ↑ij.snd
• finSigmaFinEquiv.eq_2 📋 Mathlib.Algebra.BigOperators.Fin
  (m_2 : ℕ) (n_2 : Fin m_2.succ → ℕ) : finSigmaFinEquiv = Trans.trans (Trans.trans (Trans.trans (Trans.trans finSumFinEquiv.sigmaCongrLeft.symm (Equiv.sumSigmaDistrib fun a => Fin (n_2 (finSumFinEquiv a)))) (finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma fun i => Fin (n_2 (finSumFinEquiv (Sum.inr i)))))) finSumFinEquiv) (finCongr ⋯)
• DFinsupp.sum_eq_sum_fintype 📋 Mathlib.Data.DFinsupp.BigOperators
  {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] (v : Π₀ (i : ι), β i) {f : (i : ι) → β i → γ} (hf : ∀ (i : ι), f i 0 = 0) : v.sum f = ∑ i, f i (DFinsupp.equivFunOnFintype v i)
• Sym.equivNatSumOfFintype 📋 Mathlib.Data.Finsupp.Multiset
  (α : Type u_1) [DecidableEq α] (n : ℕ) [Fintype α] : Sym α n ≃ { P // ∑ i, P i = n }
• Sym.coe_equivNatSumOfFintype_apply_apply 📋 Mathlib.Data.Finsupp.Multiset
  (α : Type u_1) [DecidableEq α] (n : ℕ) [Fintype α] (s : Sym α n) (a : α) : ↑((Sym.equivNatSumOfFintype α n) s) a = Multiset.count a ↑s
• Sym.coe_equivNatSumOfFintype_symm_apply 📋 Mathlib.Data.Finsupp.Multiset
  (α : Type u_1) [DecidableEq α] (n : ℕ) [Fintype α] (P : { P // ∑ i, P i = n }) : ↑((Sym.equivNatSumOfFintype α n).symm P) = ∑ a, ↑P a • {a}
• DirectSum.decompose_sum 📋 Mathlib.Algebra.DirectSum.Decomposition
  {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [DirectSum.Decomposition ℳ] {ι' : Type u_5} (s : Finset ι') (f : ι' → M) : (DirectSum.decompose ℳ) (∑ i ∈ s, f i) = ∑ i ∈ s, (DirectSum.decompose ℳ) (f i)
• DirectSum.decompose_symm_sum 📋 Mathlib.Algebra.DirectSum.Decomposition
  {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [DirectSum.Decomposition ℳ] {ι' : Type u_5} (s : Finset ι') (f : ι' → DirectSum ι fun i => ↥(ℳ i)) : (DirectSum.decompose ℳ).symm (∑ i ∈ s, f i) = ∑ i ∈ s, (DirectSum.decompose ℳ).symm (f i)
• DirectSum.sum_support_decompose 📋 Mathlib.Algebra.DirectSum.Decomposition
  {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [DecidableEq ι] [AddCommMonoid M] [SetLike σ M] [AddSubmonoidClass σ M] (ℳ : ι → σ) [DirectSum.Decomposition ℳ] [(i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)] (r : M) : ∑ i ∈ DFinsupp.support ((DirectSum.decompose ℳ) r), ↑(((DirectSum.decompose ℳ) r) i) = r
• Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_fst 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
  (k : ℕ) (x : Fin k → ℕ) : ((Finset.Nat.sigmaAntidiagonalTupleEquivTuple k).symm x).fst = ∑ i, x i
• Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
  (k : ℕ) (x : Fin k → ℕ) (a✝ : Fin k) : ↑((Finset.Nat.sigmaAntidiagonalTupleEquivTuple k).symm x).snd a✝ = x a✝
• HahnModule.coeff_smul 📋 Mathlib.RingTheory.HahnSeries.Multiplication
  {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [AddCommMonoid V] [SMul R V] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [Zero R] (x : HahnSeries Γ R) (y : HahnModule Γ' R V) (a : Γ') : ((HahnModule.of R).symm (x • y)).coeff a = ∑ ij ∈ Finset.VAddAntidiagonal ⋯ ⋯ a, x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2
• HahnModule.smul_coeff 📋 Mathlib.RingTheory.HahnSeries.Multiplication
  {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [AddCommMonoid V] [SMul R V] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [Zero R] (x : HahnSeries Γ R) (y : HahnModule Γ' R V) (a : Γ') : ((HahnModule.of R).symm (x • y)).coeff a = ∑ ij ∈ Finset.VAddAntidiagonal ⋯ ⋯ a, x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2
• HahnModule.coeff_smul_right 📋 Mathlib.RingTheory.HahnSeries.Multiplication
  {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [Zero R] [SMulZeroClass R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} {a : Γ'} {s : Set Γ'} (hs : s.IsPWO) (hys : ((HahnModule.of R).symm y).support ⊆ s) : ((HahnModule.of R).symm (x • y)).coeff a = ∑ ij ∈ Finset.VAddAntidiagonal ⋯ hs a, x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2
• HahnModule.smul_coeff_right 📋 Mathlib.RingTheory.HahnSeries.Multiplication
  {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [Zero R] [SMulZeroClass R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} {a : Γ'} {s : Set Γ'} (hs : s.IsPWO) (hys : ((HahnModule.of R).symm y).support ⊆ s) : ((HahnModule.of R).symm (x • y)).coeff a = ∑ ij ∈ Finset.VAddAntidiagonal ⋯ hs a, x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2
• HahnModule.coeff_smul_left 📋 Mathlib.RingTheory.HahnSeries.Multiplication
  {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [Zero R] [SMulWithZero R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} {a : Γ'} {s : Set Γ} (hs : s.IsPWO) (hxs : x.support ⊆ s) : ((HahnModule.of R).symm (x • y)).coeff a = ∑ ij ∈ Finset.VAddAntidiagonal hs ⋯ a, x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2
• HahnModule.smul_coeff_left 📋 Mathlib.RingTheory.HahnSeries.Multiplication
  {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [AddCommMonoid V] [Zero R] [SMulWithZero R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} {a : Γ'} {s : Set Γ} (hs : s.IsPWO) (hxs : x.support ⊆ s) : ((HahnModule.of R).symm (x • y)).coeff a = ∑ ij ∈ Finset.VAddAntidiagonal hs ⋯ a, x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2
• CStarMatrix.toCLM_apply_eq_sum 📋 Mathlib.Analysis.CStarAlgebra.CStarMatrix
  {m : Type u_1} {n : Type u_2} {A : Type u_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {M : CStarMatrix m n A} {v : WithCStarModule A (m → A)} : (CStarMatrix.toCLM M) v = (WithCStarModule.equiv A (n → A)).symm fun j => ∑ i, v i * M i j
• Finset.equivBitIndices_symm_apply 📋 Mathlib.Combinatorics.Colex
  (s : Finset ℕ) : Finset.equivBitIndices.symm s = ∑ i ∈ s, 2 ^ i
• AddSubgroup.leftTransversals.diff.eq_1 📋 Mathlib.GroupTheory.Transfer
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {A : Type u_2} [AddCommGroup A] (ϕ : ↥H →+ A) (S T : H.LeftTransversal) [H.FiniteIndex] : AddSubgroup.leftTransversals.diff ϕ S T = ∑ q, ϕ ⟨-↑(⋯.leftQuotientEquiv q) + ↑(⋯.leftQuotientEquiv q), ⋯⟩
• NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component 📋 Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
  {K : Type u_1} [Field K] [NumberField K] (x : (NumberField.RingOfIntegers K)ˣ) : ∑ w, (NumberField.Units.logEmbedding K) (Additive.ofMul x) w = -↑NumberField.Units.dirichletUnitTheorem.w₀.mult * Real.log (NumberField.Units.dirichletUnitTheorem.w₀ ((algebraMap (NumberField.RingOfIntegers K) K) ↑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 19971e9 serving mathlib revision 4cb993b