Loogle!

Result

Found 20 declarations mentioning Subgroup and AddMonoidHom.

• AddSubgroup.toSubgroup_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {A : Type u_7} {A₂ : Type u_8} [AddGroup A] [AddGroup A₂] (f : A →+ A₂) (s : AddSubgroup A₂) : Subgroup.comap (AddMonoidHom.toMultiplicative f) (AddSubgroup.toSubgroup s) = AddSubgroup.toSubgroup (AddSubgroup.comap f 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_toMultiplicative_ker 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {A : Type u_8} {A' : Type u_9} [AddGroup A] [AddZeroClass A'] (f : A →+ A') : (AddMonoidHom.toMultiplicative f).ker = AddSubgroup.toSubgroup f.ker
• 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_toMultiplicative_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {A : Type u_7} {A' : Type u_8} [AddGroup A] [AddGroup A'] (f : A →+ A') : (AddMonoidHom.toMultiplicative f).range = AddSubgroup.toSubgroup 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
• AddMonoidHom.coe_toMultiplicative_map 📋 Mathlib.Algebra.Module.Submodule.Map
  {G : Type u_10} {G₂ : Type u_11} [AddGroup G] [AddGroup G₂] (f : G →+ G₂) (s : AddSubgroup G) : Subgroup.map (AddMonoidHom.toMultiplicative f) (AddSubgroup.toSubgroup s) = AddSubgroup.toSubgroup (AddSubgroup.map f s)
• 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)
• IsPrimitiveRoot.zmodEquivZPowers.eq_1 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
  {R : Type u_4} {k : ℕ} [CommRing R] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) : h.zmodEquivZPowers = AddEquiv.ofBijective (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯) ⟨{ toFun := fun i => Additive.ofMul ⟨(fun x => ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩) ⋯
• NumberField.Units.logEmbeddingQuot 📋 Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
  (K : Type u_1) [Field K] [NumberField K] : Additive ((NumberField.RingOfIntegers K)ˣ ⧸ NumberField.Units.torsion K) →+ NumberField.Units.dirichletUnitTheorem.logSpace K
• NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff 📋 Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
  {K : Type u_1} [Field K] [NumberField K] {x : (NumberField.RingOfIntegers K)ˣ} : (NumberField.Units.logEmbedding K) (Additive.ofMul x) = 0 ↔ x ∈ NumberField.Units.torsion K
• NumberField.Units.logEmbeddingQuot_injective 📋 Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
  (K : Type u_1) [Field K] [NumberField K] : Function.Injective ⇑(NumberField.Units.logEmbeddingQuot K)
• NumberField.Units.logEmbeddingQuot_apply 📋 Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
  (K : Type u_1) [Field K] [NumberField K] (x : (NumberField.RingOfIntegers K)ˣ) : (NumberField.Units.logEmbeddingQuot K) (Additive.ofMul ↑x) = (NumberField.Units.logEmbedding K) (Additive.ofMul x)
• NumberField.Units.logEmbeddingEquiv_apply 📋 Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
  (K : Type u_1) [Field K] [NumberField K] (x : (NumberField.RingOfIntegers K)ˣ) : ↑((NumberField.Units.logEmbeddingEquiv K) (Additive.ofMul ↑x)) = (NumberField.Units.logEmbedding K) (Additive.ofMul x)
• SlashInvariantForm.coeHom 📋 Mathlib.NumberTheory.ModularForms.SlashInvariantForms
  {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : SlashInvariantForm Γ k →+ UpperHalfPlane → ℂ
• SlashInvariantForm.coeHom_injective 📋 Mathlib.NumberTheory.ModularForms.SlashInvariantForms
  {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : Function.Injective ⇑SlashInvariantForm.coeHom
• CuspForm.coeHom 📋 Mathlib.NumberTheory.ModularForms.Basic
  {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : CuspForm Γ k →+ UpperHalfPlane → ℂ
• ModularForm.coeHom 📋 Mathlib.NumberTheory.ModularForms.Basic
  {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} : ModularForm Γ k →+ UpperHalfPlane → ℂ
• CuspForm.coeHom_apply 📋 Mathlib.NumberTheory.ModularForms.Basic
  {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f : CuspForm Γ k) (a : UpperHalfPlane) : CuspForm.coeHom f a = f a
• ModularForm.coeHom_apply 📋 Mathlib.NumberTheory.ModularForms.Basic
  {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} (f : ModularForm Γ k) (a : UpperHalfPlane) : ModularForm.coeHom f a = f a

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 bce1d65