Loogle!

Result

Found 465 declarations mentioning AddSubgroup and AddMonoidHom. Of these, only the first 200 are shown.

• AddSubgroup.subtype 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ↥H →+ G
• AddSubgroup.inclusion 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : ↥H →+ ↥K
• AddSubgroup.subtype_injective 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] (s : AddSubgroup G) : Function.Injective ⇑s.subtype
• AddSubgroup.coe_subtype 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⇑H.subtype = Subtype.val
• AddSubgroup.subtype_apply 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {s : AddSubgroup G} (x : ↥s) : s.subtype x = ↑x
• AddSubgroup.subtype_comp_inclusion 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (hH : H ≤ K) : K.subtype.comp (AddSubgroup.inclusion hH) = H.subtype
• AddSubgroup.subtype.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.subtype = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }
• AddSubgroup.inclusion.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : AddSubgroup.inclusion h = AddMonoidHom.mk' (fun x => ⟨↑x, ⋯⟩) ⋯
• AddSubgroup.inclusion_injective 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : Function.Injective ⇑(AddSubgroup.inclusion h)
• AddSubgroup.coe_inclusion 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) (a : ↥H) : ↑((AddSubgroup.inclusion h) a) = ↑a
• AddSubgroup.inclusion_inj 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) {x y : ↥H} : (AddSubgroup.inclusion h) x = (AddSubgroup.inclusion h) y ↔ x = y
• AddSubgroup.comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : AddSubgroup G
• AddSubgroup.map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : AddSubgroup N
• AddSubgroup.comap_top 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.comap f ⊤ = ⊤
• AddSubgroup.map_bot 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.map f ⊥ = ⊥
• AddSubgroup.le_comap_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : H ≤ AddSubgroup.comap f (AddSubgroup.map f H)
• AddSubgroup.map_comap_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : AddSubgroup.map f (AddSubgroup.comap f H) ≤ H
• AddSubgroup.gc_map_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : GaloisConnection (AddSubgroup.map f) (AddSubgroup.comap f)
• AddSubgroup.comap_iInf 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ι → AddSubgroup N) : AddSubgroup.comap f (iInf s) = ⨅ i, AddSubgroup.comap f (s i)
• AddSubgroup.comap_inf 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup N) (f : G →+ N) : AddSubgroup.comap f (H ⊓ K) = AddSubgroup.comap f H ⊓ AddSubgroup.comap f K
• AddSubgroup.comap_mono 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K K' : AddSubgroup N} : K ≤ K' → AddSubgroup.comap f K ≤ AddSubgroup.comap f K'
• AddSubgroup.map_mono 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K K' : AddSubgroup G} : K ≤ K' → AddSubgroup.map f K ≤ AddSubgroup.map f K'
• AddSubgroup.map_le_iff_le_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup G} {H : AddSubgroup N} : AddSubgroup.map f K ≤ H ↔ K ≤ AddSubgroup.comap f H
• AddSubgroup.map_iSup 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ι → AddSubgroup G) : AddSubgroup.map f (iSup s) = ⨆ i, AddSubgroup.map f (s i)
• AddSubgroup.map_inf_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup G) (f : G →+ N) : AddSubgroup.map f (H ⊓ K) ≤ AddSubgroup.map f H ⊓ AddSubgroup.map f K
• AddSubgroup.map_isAddCommutative 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') [IsAddCommutative ↥H] : IsAddCommutative ↥(AddSubgroup.map f H)
• AddSubgroup.map_zero_eq_bot 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] : AddSubgroup.map 0 K = ⊥
• AddSubgroup.iSup_comap_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ι → AddSubgroup N) : ⨆ i, AddSubgroup.comap f (s i) ≤ AddSubgroup.comap f (iSup s)
• AddMonoidHom.map_closure 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (s : Set G) : AddSubgroup.map f (AddSubgroup.closure s) = AddSubgroup.closure (⇑f '' s)
• AddSubgroup.map_sup 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup G) (f : G →+ N) : AddSubgroup.map f (H ⊔ K) = AddSubgroup.map f H ⊔ AddSubgroup.map f K
• AddSubgroup.map_top_of_surjective 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (h : Function.Surjective ⇑f) : AddSubgroup.map f ⊤ = ⊤
• AddSubgroup.coe_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup N) (f : G →+ N) : ↑(AddSubgroup.comap f K) = ⇑f ⁻¹' ↑K
• AddSubgroup.coe_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (K : AddSubgroup G) : ↑(AddSubgroup.map f K) = ⇑f '' ↑K
• AddMonoidHom.closure_preimage_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (s : Set N) : AddSubgroup.closure (⇑f ⁻¹' s) ≤ AddSubgroup.comap f (AddSubgroup.closure s)
• AddSubgroup.comap_sup_comap_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup N) (f : G →+ N) : AddSubgroup.comap f H ⊔ AddSubgroup.comap f K ≤ AddSubgroup.comap f (H ⊔ K)
• AddSubgroup.comap_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {P : Type u_6} [AddGroup P] (K : AddSubgroup P) (g : N →+ P) (f : G →+ N) : AddSubgroup.comap f (AddSubgroup.comap g K) = AddSubgroup.comap (g.comp f) K
• AddSubgroup.map_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] {P : Type u_6} [AddGroup P] (g : N →+ P) (f : G →+ N) : AddSubgroup.map g (AddSubgroup.map f K) = AddSubgroup.map (g.comp f) K
• AddSubgroup.mem_map_of_mem 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {K : AddSubgroup G} {x : G} (hx : x ∈ K) : f x ∈ AddSubgroup.map f K
• AddSubgroup.mem_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {K : AddSubgroup N} {f : G →+ N} {x : G} : x ∈ AddSubgroup.comap f K ↔ f x ∈ K
• AddSubgroup.map_iInf 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} [Nonempty ι] (f : G →+ N) (hf : Function.Injective ⇑f) (s : ι → AddSubgroup G) : AddSubgroup.map f (iInf s) = ⨅ i, AddSubgroup.map f (s i)
• AddSubgroup.map_inf 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) : AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.map f K
• AddSubgroup.map_inf_eq 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) : AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.map f K
• AddSubgroup.mem_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup G} {y : N} : y ∈ AddSubgroup.map f K ↔ ∃ x ∈ K, f x = y
• AddSubgroup.surjOn_iff_le_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} {K : AddSubgroup N} : Set.SurjOn ⇑f ↑H ↑K ↔ K ≤ AddSubgroup.map f H
• AddSubgroup.apply_coe_mem_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (K : AddSubgroup G) (x : ↥K) : f ↑x ∈ AddSubgroup.map f K
• AddSubgroup.map_toAddSubmonoid 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (K : AddSubgroup G) : (AddSubgroup.map f K).toAddSubmonoid = AddSubmonoid.map f K.toAddSubmonoid
• AddSubgroup.equivMapOfInjective 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) : ↥H ≃+ ↥(AddSubgroup.map f H)
• AddSubgroup.comap_injective_isAddCommutative 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G' →+ G} (hf : Function.Injective ⇑f) [IsAddCommutative ↥H] : IsAddCommutative ↥(AddSubgroup.comap f H)
• AddSubgroup.comap.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : AddSubgroup.comap f H = { carrier := ⇑f ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
• AddSubgroup.map.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : AddSubgroup.map f H = { carrier := ⇑f '' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
• AddSubgroup.codisjoint_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Surjective ⇑f) {H K : AddSubgroup G} (h : Codisjoint H K) : Codisjoint (AddSubgroup.map f H) (AddSubgroup.map f K)
• AddSubgroup.disjoint_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {H K : AddSubgroup G} (h : Disjoint H K) : Disjoint (AddSubgroup.map f H) (AddSubgroup.map f K)
• AddSubgroup.mem_map_iff_mem 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {K : AddSubgroup G} {x : G} : f x ∈ AddSubgroup.map f K ↔ x ∈ K
• AddMonoidHom.addSubgroupComap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H' : AddSubgroup G') : ↥(AddSubgroup.comap f H') →+ ↥H'
• AddMonoidHom.addSubgroupMap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) : ↥H →+ ↥(AddSubgroup.map f H)
• AddSubgroup.map_eq_comap_of_inverse 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (hl : Function.LeftInverse ⇑g ⇑f) (hr : Function.RightInverse ⇑g ⇑f) (H : AddSubgroup G) : AddSubgroup.map f H = AddSubgroup.comap g H
• AddSubgroup.equivMapOfInjective.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) : H.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_add' := ⋯ }
• AddMonoidHom.addSubgroupComap.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H' : AddSubgroup G') : f.addSubgroupComap H' = f.addSubmonoidComap H'.toAddSubmonoid
• AddMonoidHom.addSubgroupMap.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) : f.addSubgroupMap H = f.addSubmonoidMap H.toAddSubmonoid
• AddSubgroup.comap_toAddSubmonoid 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (e : G ≃+ N) (s : AddSubgroup N) : (AddSubgroup.comap (↑e) s).toAddSubmonoid = AddSubmonoid.comap e.toAddMonoidHom s.toAddSubmonoid
• AddSubgroup.coe_addSubgroupOf 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : ↑(H.addSubgroupOf K) = ⇑K.subtype ⁻¹' ↑H
• AddSubgroup.coe_equivMapOfInjective_apply 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) (h : ↥H) : ↑((H.equivMapOfInjective f hf) h) = f ↑h
• 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)
• AddMonoidHom.addSubgroupMap_surjective 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) : Function.Surjective ⇑(f.addSubgroupMap H)
• AddMonoidHom.addSubgroupComap_surjective_of_surjective 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H' : AddSubgroup G') (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(f.addSubgroupComap H')
• AddMonoidHom.addSubgroupMap_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) (x : ↥H.toAddSubmonoid) : ↑((f.addSubgroupMap H) x) = f ↑x
• AddMonoidHom.addSubgroupComap_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H' : AddSubgroup G') (x : ↥(AddSubmonoid.comap f H'.toAddSubmonoid)) : ↑((f.addSubgroupComap H') x) = f ↑x
• AddMonoidHom.ker 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : AddSubgroup G
• AddMonoidHom.range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup N
• AddMonoidHom.eqLocus 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] (f g : G →+ M) : AddSubgroup G
• AddMonoidHom.decidableMemKer 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] [DecidableEq M] (f : G →+ M) : DecidablePred fun x => x ∈ f.ker
• AddMonoidHom.eqLocus_same 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.eqLocus f = ⊤
• AddMonoidHom.ker_toHomAddUnits 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_8} [AddMonoid M] (f : G →+ M) : f.toHomAddUnits.ker = f.ker
• AddMonoidHom.range_eq_map 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.range = AddSubgroup.map f ⊤
• AddMonoidHom.comap_bot 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.comap f ⊥ = f.ker
• AddSubgroup.map_le_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : AddSubgroup.map f H ≤ f.range
• AddSubgroup.map_comap_eq 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : AddSubgroup.map f (AddSubgroup.comap f H) = f.range ⊓ H
• AddSubgroup.ker_le_comap 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : f.ker ≤ AddSubgroup.comap f H
• AddMonoidHom.range_isAddCommutative 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_7} [AddCommGroup G] {N : Type u_8} [AddGroup N] (f : G →+ N) : IsAddCommutative ↥f.range
• AddMonoidHom.ker_zero 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] : AddMonoidHom.ker 0 = ⊤
• AddSubgroup.map_comap_eq_self 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup N} (h : H ≤ f.range) : AddSubgroup.map f (AddSubgroup.comap f H) = H
• AddSubgroup.comap_map_eq_self 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} (h : f.ker ≤ H) : AddSubgroup.comap f (AddSubgroup.map f H) = H
• AddMonoidHom.eqLocus.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] (f g : G →+ M) : f.eqLocus g = { toAddSubmonoid := f.eqLocusM g, neg_mem' := ⋯ }
• AddMonoidHom.ker_eq_bot_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : f.ker = ⊥ ↔ Function.Injective ⇑f
• AddSubgroup.map_eq_bot_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} : AddSubgroup.map f H = ⊥ ↔ H ≤ f.ker
• AddSubgroup.comap_map_eq 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : AddSubgroup.comap f (AddSubgroup.map f H) = H ⊔ f.ker
• AddMonoidHom.range_zero 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] : AddMonoidHom.range 0 = ⊥
• AddMonoidHom.ker.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : f.ker = { toAddSubmonoid := AddMonoidHom.mker f, neg_mem' := ⋯ }
• AddMonoidHom.ker_prod 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_8} {N : Type u_9} [AddZeroClass M] [AddZeroClass N] (f : G →+ M) (g : G →+ N) : (f.prod g).ker = f.ker ⊓ g.ker
• AddSubgroup.comap_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Surjective ⇑f) : Function.Injective (AddSubgroup.comap f)
• AddSubgroup.map_eq_range_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} : AddSubgroup.map f H = f.range ↔ Codisjoint H f.ker
• AddSubgroup.map_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Injective ⇑f) : Function.Injective (AddSubgroup.map f)
• AddMonoidHom.mem_ker 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] {f : G →+ M} {x : G} : x ∈ f.ker ↔ f x = 0
• AddMonoidHom.coe_ker 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : ↑f.ker = ⇑f ⁻¹' {0}
• AddMonoidHom.comap_ker 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {P : Type u_8} [AddZeroClass P] (g : N →+ P) (f : G →+ N) : AddSubgroup.comap f g.ker = (g.comp f).ker
• AddMonoidHom.coe_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : ↑f.range = Set.range ⇑f
• AddMonoidHom.range_eq_top_of_surjective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] (f : G →+ N) (hf : Function.Surjective ⇑f) : f.range = ⊤
• AddMonoidHom.range_eq_top 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] {f : G →+ N} : f.range = ⊤ ↔ Function.Surjective ⇑f
• AddSubgroup.comap_map_eq_self_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Injective ⇑f) (H : AddSubgroup G) : AddSubgroup.comap f (AddSubgroup.map f H) = H
• AddSubgroup.map_comap_eq_self_of_surjective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Surjective ⇑f) (H : AddSubgroup N) : AddSubgroup.map f (AddSubgroup.comap f H) = H
• AddMonoidHom.ker_eq_top_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] {f : G →+ M} : f.ker = ⊤ ↔ f = 0
• AddSubgroup.comap_le_comap_of_le_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K L : AddSubgroup N} (hf : K ≤ f.range) : AddSubgroup.comap f K ≤ AddSubgroup.comap f L ↔ K ≤ L
• AddMonoidHom.mem_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {y : N} : y ∈ f.range ↔ ∃ x, f x = y
• AddMonoidHom.map_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} {P : Type u_6} [AddGroup N] [AddGroup P] (g : N →+ P) (f : G →+ N) : AddSubgroup.map g f.range = (g.comp f).range
• AddMonoidHom.range_comp 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} {P : Type u_6} [AddGroup N] [AddGroup P] (g : N →+ P) (f : G →+ N) : (g.comp f).range = AddSubgroup.map g f.range
• AddMonoidHom.restrict_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) (f : G →+ N) : (f.restrict K).range = AddSubgroup.map f K
• AddMonoidHom.range.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.range = (AddSubgroup.map f ⊤).copy (Set.range ⇑f) ⋯
• AddSubgroup.map_eq_bot_iff_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} (hf : Function.Injective ⇑f) : AddSubgroup.map f H = ⊥ ↔ H = ⊥
• AddSubgroup.map_le_map_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H K : AddSubgroup G} : AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ≤ K ⊔ f.ker
• AddSubgroup.map_injective_of_ker_le 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {H K : AddSubgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K) (hf : AddSubgroup.map f H = AddSubgroup.map f K) : H = K
• AddMonoidHom.ker_restrict 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {M : Type u_7} [AddZeroClass M] (f : G →+ M) : (f.restrict K).ker = f.ker.addSubgroupOf K
• AddSubgroup.map_eq_map_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H K : AddSubgroup G} : AddSubgroup.map f H = AddSubgroup.map f K ↔ H ⊔ f.ker = K ⊔ f.ker
• AddMonoidHom.ofInjective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) : G ≃+ ↥f.range
• AddMonoidHom.sub_mem_ker_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) {x y : G} : x - y ∈ f.ker ↔ f x = f y
• AddSubgroup.comap_le_comap_of_surjective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K L : AddSubgroup N} (hf : Function.Surjective ⇑f) : AddSubgroup.comap f K ≤ AddSubgroup.comap f L ↔ K ≤ L
• AddSubgroup.comap_lt_comap_of_surjective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K L : AddSubgroup N} (hf : Function.Surjective ⇑f) : AddSubgroup.comap f K < AddSubgroup.comap f L ↔ K < L
• AddSubgroup.map_le_map_iff_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {H K : AddSubgroup G} : AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ≤ K
• AddSubgroup.map_lt_map_iff_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {H K : AddSubgroup G} : AddSubgroup.map f H < AddSubgroup.map f K ↔ H < K
• AddMonoidHom.range_eq_bot_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {f : G →+ G'} : f.range = ⊥ ↔ f = 0
• AddSubgroup.comap_sup_eq_of_le_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {H K : AddSubgroup N} (hH : H ≤ f.range) (hK : K ≤ f.range) : AddSubgroup.comap f H ⊔ AddSubgroup.comap f K = AddSubgroup.comap f (H ⊔ K)
• AddSubgroup.map_le_map_iff' 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H K : AddSubgroup G} : AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker
• AddMonoidHom.eq_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) {x y : G} : f x = f y ↔ -y + x ∈ f.ker
• AddSubgroup.comap_sup_eq 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H K : AddSubgroup N) (hf : Function.Surjective ⇑f) : AddSubgroup.comap f H ⊔ AddSubgroup.comap f K = AddSubgroup.comap f (H ⊔ K)
• AddMonoidHom.eq_of_eqOn_top 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] {f g : G →+ M} (h : Set.EqOn ⇑f ⇑g ↑⊤) : f = g
• AddMonoidHom.ker_rangeRestrict 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.rangeRestrict.ker = f.ker
• AddMonoidHom.eq_of_eqOn_dense 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] {s : Set G} (hs : AddSubgroup.closure s = ⊤) {f g : G →+ M} (h : Set.EqOn (⇑f) (⇑g) s) : f = g
• AddMonoidHom.range_le_ker_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {M : Type u_7} [AddZeroClass M] (f : G →+ G') (g : G' →+ M) : f.range ≤ g.ker ↔ g.comp f = 0
• AddMonoidHom.rangeRestrict 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : G →+ ↥f.range
• AddMonoidHom.ker_codRestrict 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {S : Type u_8} [SetLike S N] [AddSubmonoidClass S N] (f : G →+ N) (s : S) (h : ∀ (x : G), f x ∈ s) : (f.codRestrict s h).ker = f.ker
• AddMonoidHom.decidableMemKer.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] [DecidableEq M] (f : G →+ M) (x : G) : f.decidableMemKer x = decidable_of_iff (f x = 0) ⋯
• AddMonoidHom.ofLeftInverse 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse ⇑g ⇑f) : G ≃+ ↥f.range
• AddSubgroup.ker_addSubgroupMap 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) : (f.addSubgroupMap H).ker = f.ker.addSubgroupOf H
• AddMonoidHom.rangeRestrict.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.rangeRestrict = f.codRestrict f.range ⋯
• AddMonoidHom.subtype_comp_rangeRestrict 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.range.subtype.comp f.rangeRestrict = f
• AddMonoidHom.eqOn_closure 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] {f g : G →+ M} {s : Set G} (h : Set.EqOn (⇑f) (⇑g) s) : Set.EqOn ⇑f ⇑g ↑(AddSubgroup.closure s)
• AddMonoidHom.ofInjective_apply 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {x : G} : ↑((AddMonoidHom.ofInjective hf) x) = f x
• AddMonoidHom.addSubgroupOf_range_eq_of_le 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G₁ : Type u_7} {G₂ : Type u_8} [AddGroup G₁] [AddGroup G₂] {K : AddSubgroup G₂} (f : G₁ →+ G₂) (h : f.range ≤ K) : f.range.addSubgroupOf K = (f.codRestrict K ⋯).range
• AddMonoidHom.rangeRestrict_surjective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : Function.Surjective ⇑f.rangeRestrict
• 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
• AddMonoidHom.ofInjective.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) : AddMonoidHom.ofInjective hf = AddEquiv.ofBijective (f.codRestrict f.range ⋯) ⋯
• AddMonoidHom.coe_rangeRestrict 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (g : G) : ↑(f.rangeRestrict g) = f g
• AddMonoidHom.rangeRestrict_injective_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} : Function.Injective ⇑f.rangeRestrict ↔ Function.Injective ⇑f
• AddMonoidHom.ofLeftInverse_apply 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse ⇑g ⇑f) (x : G) : ↑((AddMonoidHom.ofLeftInverse h) x) = f x
• AddMonoidHom.apply_ofInjective_symm 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) (x : ↥f.range) : f ((AddMonoidHom.ofInjective hf).symm x) = ↑x
• AddMonoidHom.coe_comp_rangeRestrict 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : Subtype.val ∘ ⇑f.rangeRestrict = ⇑f
• 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
• AddSubgroup.closure_preimage_eq_top 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] (s : Set G) : AddSubgroup.closure (⇑(AddSubgroup.closure s).subtype ⁻¹' s) = ⊤
• 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.ofLeftInverse_symm_apply 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse ⇑g ⇑f) (x : ↥f.range) : (AddMonoidHom.ofLeftInverse h).symm x = g ↑x
• AddMonoidHom.ker_comp_addEquiv 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {P : Type u_8} [AddZeroClass P] (g : N →+ P) (iso : G ≃+ N) : (g.comp ↑iso).ker = AddSubgroup.map (↑iso.symm) g.ker
• AddMonoidHom.ofLeftInverse.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse ⇑g ⇑f) : AddMonoidHom.ofLeftInverse h = { toFun := ⇑f.rangeRestrict, invFun := ⇑g ∘ ⇑f.range.subtype, left_inv := h, right_inv := ⋯, map_add' := ⋯ }
• AddSubgroup.normal_comap 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup N} [nH : H.Normal] (f : G →+ N) : (AddSubgroup.comap f H).Normal
• AddSubgroup.Normal.comap 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup N} (hH : H.Normal) (f : G →+ N) : (AddSubgroup.comap f H).Normal
• AddSubgroup.le_normalizer_comap 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : Type u_5} [AddGroup N] (f : N →+ G) : AddSubgroup.comap f H.normalizer ≤ (AddSubgroup.comap f H).normalizer
• AddSubgroup.le_normalizer_map 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.map f H.normalizer ≤ (AddSubgroup.map f H).normalizer
• AddSubgroup.comap_normalizer_eq_of_le_range 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : Type u_5} [AddGroup N] {f : N →+ G} (h : H ≤ f.range) : AddSubgroup.comap f H.normalizer = (AddSubgroup.comap f H).normalizer
• AddSubgroup.Normal.map 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} (h : H.Normal) (f : G →+ N) (hf : Function.Surjective ⇑f) : (AddSubgroup.map f H).Normal
• AddSubgroup.comap_normalizer_eq_of_surjective 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : N →+ G} (hf : Function.Surjective ⇑f) : AddSubgroup.comap f H.normalizer = (AddSubgroup.comap f H).normalizer
• AddSubgroup.map_normalizer_eq_of_bijective 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} (hf : Function.Bijective ⇑f) : AddSubgroup.map f H.normalizer = (AddSubgroup.map f H).normalizer
• AddMonoidHom.prodMap_comap_prod 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {G' : Type u_8} {N' : Type u_9} [AddGroup G'] [AddGroup N'] (f : G →+ N) (g : G' →+ N') (S : AddSubgroup N) (S' : AddSubgroup N') : AddSubgroup.comap (f.prodMap g) (S.prod S') = (AddSubgroup.comap f S).prod (AddSubgroup.comap g S')
• AddMonoidHom.ker_prodMap 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {G' : Type u_8} {N' : Type u_9} [AddGroup G'] [AddGroup N'] (f : G →+ N) (g : G' →+ N') : (f.prodMap g).ker = f.ker.prod g.ker
• AddMonoidHom.liftOfRightInverseAux 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_neg : G₂ → G₁) (hf : Function.RightInverse f_neg ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) : G₂ →+ G₃
• AddMonoidHom.liftOfSurjective 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (hf : Function.Surjective ⇑f) : { g // f.ker ≤ g.ker } ≃ (G₂ →+ G₃)
• AddMonoidHom.liftOfRightInverse 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_neg : G₂ → G₁) (hf : Function.RightInverse f_neg ⇑f) : { g // f.ker ≤ g.ker } ≃ (G₂ →+ G₃)
• AddMonoidHom.liftOfSurjective.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (hf : Function.Surjective ⇑f) : f.liftOfSurjective hf = f.liftOfRightInverse (Function.surjInv hf) ⋯
• AddMonoidHom.liftOfRightInverseAux.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) : f.liftOfRightInverseAux f_inv hf g hg = { toFun := fun b => g (f_inv b), map_zero' := ⋯, map_add' := ⋯ }
• AddMonoidHom.liftOfRightInverseAux_comp_apply 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_neg : G₂ → G₁) (hf : Function.RightInverse f_neg ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) (x : G₁) : (f.liftOfRightInverseAux f_neg hf g hg) (f x) = g x
• AddMonoidHom.liftOfRightInverse.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) : f.liftOfRightInverse f_inv hf = { toFun := fun g => f.liftOfRightInverseAux f_inv hf ↑g ⋯, invFun := fun φ => ⟨φ.comp f, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
• AddMonoidHom.liftOfRightInverse_comp 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_neg : G₂ → G₁) (hf : Function.RightInverse f_neg ⇑f) (g : { g // f.ker ≤ g.ker }) : ((f.liftOfRightInverse f_neg hf) g).comp f = ↑g
• AddMonoidHom.eq_liftOfRightInverse 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_neg : G₂ → G₁) (hf : Function.RightInverse f_neg ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) (h : G₂ →+ G₃) (hh : h.comp f = g) : h = (f.liftOfRightInverse f_neg hf) ⟨g, hg⟩
• AddMonoidHom.liftOfRightInverse_comp_apply 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_neg : G₂ → G₁) (hf : Function.RightInverse f_neg ⇑f) (g : { g // f.ker ≤ g.ker }) (x : G₁) : ((f.liftOfRightInverse f_neg hf) g) (f x) = ↑g x
• AddMonoidHom.map_zmultiples 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_3} [AddGroup N] (f : G →+ N) (x : G) : AddSubgroup.map f (AddSubgroup.zmultiples x) = AddSubgroup.zmultiples (f x)
• AddSubgroup.map_centralizer_le_centralizer_image 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (s : Set G) (f : G →+ G') : AddSubgroup.map f (AddSubgroup.centralizer s) ≤ AddSubgroup.centralizer (⇑f '' s)
• FreeAddGroup.range_lift_eq_closure 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α : Type u} {β : Type v} [AddGroup β] {f : α → β} : (FreeAddGroup.lift f).range = AddSubgroup.closure (Set.range f)
• FreeAddGroup.range_lift_le 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α : Type u} {β : Type v} [AddGroup β] {f : α → β} {s : AddSubgroup β} (H : Set.range f ⊆ ↑s) : (FreeAddGroup.lift f).range ≤ s
• FreeAddGroup.closure_eq_range 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {β : Type v} [AddGroup β] (s : Set β) : AddSubgroup.closure s = (FreeAddGroup.lift Subtype.val).range
• QuotientAddGroup.mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : G →+ G ⧸ N
• QuotientAddGroup.mk'.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : QuotientAddGroup.mk' N = AddMonoidHom.mk' QuotientAddGroup.mk ⋯
• QuotientAddGroup.lift 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] (φ : G →+ M) (HN : N ≤ φ.ker) : G ⧸ N →+ M
• QuotientAddGroup.ker_lift 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] (φ : G →+ M) (HN : N ≤ φ.ker) : (QuotientAddGroup.lift N φ HN).ker = AddSubgroup.map (QuotientAddGroup.mk' N) φ.ker
• QuotientAddGroup.lift.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] (φ : G →+ M) (HN : N ≤ φ.ker) : QuotientAddGroup.lift N φ HN = (QuotientAddGroup.con N).lift φ ⋯
• QuotientAddGroup.lift_comp_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] (φ : G →+ M) (HN : N ≤ φ.ker) : (QuotientAddGroup.lift N φ HN).comp (QuotientAddGroup.mk' N) = φ
• QuotientAddGroup.mk'_surjective 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : Function.Surjective ⇑(QuotientAddGroup.mk' N)
• QuotientAddGroup.coe_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : ⇑(QuotientAddGroup.mk' N) = QuotientAddGroup.mk
• QuotientAddGroup.map 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) : G ⧸ N →+ H ⧸ M
• QuotientAddGroup.mk'_apply 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (x : G) : (QuotientAddGroup.mk' N) x = ↑x
• QuotientAddGroup.liftEquiv 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] {φ : G →+ H} (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker) : G ⧸ N ≃+ H
• QuotientAddGroup.ker_map 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) : (QuotientAddGroup.map N M f h).ker = AddSubgroup.map (QuotientAddGroup.mk' N) (AddSubgroup.comap f M)
• QuotientAddGroup.lift_mk 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] {φ : G →+ M} (HN : N ≤ φ.ker) (g : G) : (QuotientAddGroup.lift N φ HN) ↑g = φ g
• QuotientAddGroup.lift_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] {φ : G →+ M} (HN : N ≤ φ.ker) (g : G) : (QuotientAddGroup.lift N φ HN) ↑g = φ g
• QuotientAddGroup.lift_quot_mk 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] {φ : G →+ M} (HN : N ≤ φ.ker) (g : G) : (QuotientAddGroup.lift N φ HN) (Quot.mk (⇑(QuotientAddGroup.leftRel N)) g) = φ g
• QuotientAddGroup.lift_surjective_of_surjective 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] (φ : G →+ M) (hφ : Function.Surjective ⇑φ) (HN : N ≤ φ.ker) : Function.Surjective ⇑(QuotientAddGroup.lift N φ HN)
• QuotientAddGroup.map_id 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (h : N ≤ AddSubgroup.comap (AddMonoidHom.id G) N := ⋯) : QuotientAddGroup.map N N (AddMonoidHom.id G) h = AddMonoidHom.id (G ⧸ N)
• QuotientAddGroup.map.congr_simp 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup H) [M.Normal] (f f✝ : G →+ H) (e_f : f = f✝) (h : N ≤ AddSubgroup.comap f M) : QuotientAddGroup.map N M f h = QuotientAddGroup.map N M f✝ ⋯
• QuotientAddGroup.map.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) : QuotientAddGroup.map N M f h = QuotientAddGroup.lift N ((QuotientAddGroup.mk' M).comp f) ⋯
• QuotientAddGroup.mk'_eq_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {x y : G} : (QuotientAddGroup.mk' N) x = (QuotientAddGroup.mk' N) y ↔ ∃ z ∈ N, x + z = y
• QuotientAddGroup.map_id_apply 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (h : N ≤ AddSubgroup.comap (AddMonoidHom.id G) N := ⋯) (x : G ⧸ N) : (QuotientAddGroup.map N N (AddMonoidHom.id G) h) x = x
• QuotientAddGroup.addMonoidHom_ext 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {M : Type u_4} [AddGroup G] [AddMonoid M] (N : AddSubgroup G) [nN : N.Normal] ⦃f g : G ⧸ N →+ M⦄ (h : f.comp (QuotientAddGroup.mk' N) = g.comp (QuotientAddGroup.mk' N)) : f = g

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 36960b0 serving mathlib revision 9a4cf1d