Loogle!

Result

Found 14 declarations mentioning Additive, Group, and Subgroup.

• AddSubgroup.toSubgroup' 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] : AddSubgroup (Additive G) ≃o Subgroup G
• Subgroup.toAddSubgroup 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] : Subgroup G ≃o AddSubgroup (Additive G)
• AddSubgroup.toSubgroup'_closure 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (S : Set (Additive G)) : AddSubgroup.toSubgroup' (AddSubgroup.closure S) = Subgroup.closure (⇑Additive.ofMul ⁻¹' S)
• Subgroup.toAddSubgroup_closure 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (S : Set G) : Subgroup.toAddSubgroup (Subgroup.closure S) = AddSubgroup.closure (⇑Additive.toMul ⁻¹' S)
• Subgroup.coe_toAddSubgroup_apply 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (S : Subgroup G) : ↑(Subgroup.toAddSubgroup S) = ⇑Additive.toMul ⁻¹' ↑S
• Subgroup.coe_toAddSubgroup_symm_apply 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (S : AddSubgroup (Additive G)) : ↑((RelIso.symm Subgroup.toAddSubgroup) S) = ⇑Multiplicative.toAdd ⁻¹' ↑S
• Subgroup.toAddSubgroup_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {G₂ : Type u_7} [Group G₂] (f : G →* G₂) (s : Subgroup G₂) : AddSubgroup.comap (MonoidHom.toAdditive f) (Subgroup.toAddSubgroup s) = Subgroup.toAddSubgroup (Subgroup.comap f s)
• MonoidHom.coe_toAdditive_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') : (MonoidHom.toAdditive f).range = Subgroup.toAddSubgroup f.range
• MonoidHom.coe_toAdditive_ker 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') : (MonoidHom.toAdditive f).ker = Subgroup.toAddSubgroup f.ker
• MonoidHom.coe_toAdditive_map 📋 Mathlib.Algebra.Module.Submodule.Map
  {G : Type u_10} {G₂ : Type u_11} [Group G] [Group G₂] (f : G →* G₂) (s : Subgroup G) : AddSubgroup.map (MonoidHom.toAdditive f) (Subgroup.toAddSubgroup s) = Subgroup.toAddSubgroup (Subgroup.map f s)
• ofMul_image_zpowers_eq_zmultiples_ofMul 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
  {G : Type u_1} [Group G] {x : G} : ⇑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (Additive.ofMul x))
• Subgroup.fg_iff_add_fg 📋 Mathlib.GroupTheory.Finiteness
  {G : Type u_3} [Group G] (P : Subgroup G) : P.FG ↔ (Subgroup.toAddSubgroup P).FG
• Subgroup.index_toAddSubgroup 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} [Group G] {H : Subgroup G} : (Subgroup.toAddSubgroup H).index = H.index
• Subgroup.relindex_toAddSubgroup 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} [Group G] {H K : Subgroup G} : (Subgroup.toAddSubgroup H).relindex (Subgroup.toAddSubgroup K) = H.relindex K

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