Loogle!

Result

Found 11 declarations mentioning Equiv, Fintype, and Finset.sum.

• Equiv.sum_comp 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] (e : ι ≃ κ) (g : κ → M) : ∑ i, g (e i) = ∑ i, g i
• Fintype.sum_equiv 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
  {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] (e : ι ≃ κ) (f : ι → M) (g : κ → M) (h : ∀ (x : ι), f x = g (e x)) : ∑ x, f x = ∑ x, g x
• Finsupp.equivFunOnFinite_symm_sum 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
  {α : Type u_1} {M : Type u_8} [Fintype α] [AddCommMonoid M] (f : α → M) : ((Finsupp.equivFunOnFinite.symm f).sum fun x n => n) = ∑ a, f a
• 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
• 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)
• Matrix.sum_sum_single 📋 Mathlib.Data.Matrix.Basis
  {m : Type u_2} {n : Type u_3} {α : Type u_7} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] [Fintype m] [Fintype n] (x : m → n → α) : ∑ i, ∑ j, Matrix.single i j (x i j) = Matrix.of x
• 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}
• OrthonormalBasis.equiv_apply 📋 Mathlib.Analysis.InnerProductSpace.PiL2
  {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {E' : Type u_7} [Fintype ι'] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (b : OrthonormalBasis ι 𝕜 E) (b' : OrthonormalBasis ι' 𝕜 E') (e : ι ≃ ι') (x : E) : (b.equiv b' e) x = ∑ i, (b.repr x).ofLp i • b' (e i)
• 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

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 6ff4759 serving mathlib revision 76f94b4