Loogle!

Result

Found 439 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.coeSubtype 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⇑H.subtype = Subtype.val
• 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.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.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.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_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.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_isCommutative 📋 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)
• 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_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_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.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_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.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
• 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.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)
• 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
• 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.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.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.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.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.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_injective_isCommutative 📋 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.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
• 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.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' := ⋯ }
• 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
• 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)
• 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.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_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
• AddMonoidHom.ker_zero 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] : AddMonoidHom.ker 0 = ⊤
• 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.range_isCommutative 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_7} [AddCommGroup G] {N : Type u_8} [AddGroup N] (f : G →+ N) : IsAddCommutative ↥f.range
• 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
• 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.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.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' := ⋯ }
• 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 📋 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.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.range_zero 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] : AddMonoidHom.range 0 = ⊥
• 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}
• 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_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.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.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
• AddMonoidHom.ker_sum 📋 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_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
• 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
• 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.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.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.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.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 = ⊥
• 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
• 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
• 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
• 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
• 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
• 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
• 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.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.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.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
• 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
• 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.ker_restrict 📋 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).ker = f.ker.addSubgroupOf K
• 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.sub_mem_ker_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {x y : G} : x - y ∈ f.ker ↔ f x = f y
• 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
• 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.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
• 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.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.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.range_le_ker_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} {G' : Type u_2} {G'' : Type u_3} [AddGroup G] [AddGroup G'] [AddGroup G''] (f : G →+ G') (g : G' →+ G'') : f.range ≤ g.ker ↔ g.comp f = 0
• 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_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_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.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.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.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
• 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
• 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
• 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
• 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
• 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) = ⊤
• 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.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.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' := ⋯ }
• 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)
• Submodule.AddMonoidHom.coe_toIntLinearMap_comap 📋 Mathlib.Algebra.Module.Submodule.Map
  {A : Type u_10} {A₂ : Type u_11} [AddCommGroup A] [AddCommGroup A₂] (f : A →+ A₂) (s : AddSubgroup A₂) : Submodule.comap f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.comap f s)
• AddMonoidHom.coe_toIntLinearMap_map 📋 Mathlib.Algebra.Module.Submodule.Map
  {A : Type u_10} {A₂ : Type u_11} [AddCommGroup A] [AddCommGroup A₂] (f : A →+ A₂) (s : AddSubgroup A) : Submodule.map f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.map f s)
• AddMonoidHom.coe_toIntLinearMap_ker 📋 Mathlib.Algebra.Module.Submodule.Ker
  {M : Type u_12} {M₂ : Type u_13} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : LinearMap.ker f.toIntLinearMap = AddSubgroup.toIntSubmodule f.ker
• 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_injective_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.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.sumMap_comap_sum 📋 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.ker_sumMap 📋 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_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑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_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑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_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_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) (x : G₁) : (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x
• 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.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_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g // f.ker ≤ g.ker }) : ((f.liftOfRightInverse f_inv 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_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) (h : G₂ →+ G₃) (hh : h.comp f = g) : h = (f.liftOfRightInverse f_inv 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_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g // f.ker ≤ g.ker }) (x : G₁) : ((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x
• AddMonoidHom.coe_toIntLinearMap_range 📋 Mathlib.Algebra.Module.Submodule.Range
  {M : Type u_11} {M₂ : Type u_12} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : LinearMap.range f.toIntLinearMap = AddSubgroup.toIntSubmodule f.range
• 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)
• AddMonoidHom.graph 📋 Mathlib.Algebra.Group.Graph
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) : AddSubgroup (G × H)
• AddMonoidHom.graph.eq_1 📋 Mathlib.Algebra.Group.Graph
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) : f.graph = { toAddSubmonoid := f.mgraph, neg_mem' := ⋯ }
• AddMonoidHom.graph_eq_range_prod 📋 Mathlib.Algebra.Group.Graph
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) : f.graph = ((AddMonoidHom.id G).prod f).range
• AddMonoidHom.coe_graph 📋 Mathlib.Algebra.Group.Graph
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) : ↑f.graph = {x | f x.1 = x.2}
• AddMonoidHom.mem_graph 📋 Mathlib.Algebra.Group.Graph
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G →+ H} {x : G × H} : x ∈ f.graph ↔ f x.1 = x.2
• AddMonoidHom.exists_range_eq_graph 📋 Mathlib.Algebra.Group.Graph
  {G : Type u_1} {H : Type u_2} {I : Type u_3} [AddGroup G] [AddGroup H] [AddGroup I] {f : G →+ H × I} (hf₁ : Function.Surjective (Prod.fst ∘ ⇑f)) (hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) : ∃ f', f.range = f'.graph
• AddMonoidHom.exists_addEquiv_range_eq_graph 📋 Mathlib.Algebra.Group.Graph
  {G : Type u_1} {H : Type u_2} {I : Type u_3} [AddGroup G] [AddGroup H] [AddGroup I] {f : G →+ H × I} (hf₁ : Function.Surjective (Prod.fst ∘ ⇑f)) (hf₂ : Function.Surjective (Prod.snd ∘ ⇑f)) (hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) : ∃ e, f.range = e.toAddMonoidHom.graph
• AddSubgroup.exists_eq_graph 📋 Mathlib.Algebra.Group.Graph
  {H : Type u_2} {I : Type u_3} [AddGroup H] [AddGroup I] {G : AddSubgroup (H × I)} (hG₁ : Function.Bijective (Prod.fst ∘ ⇑G.subtype)) : ∃ f, G = f.graph
• AddSubgroup.exists_addEquiv_eq_graph 📋 Mathlib.Algebra.Group.Graph
  {H : Type u_2} {I : Type u_3} [AddGroup H] [AddGroup I] {G : AddSubgroup (H × I)} (hG₁ : Function.Bijective (Prod.fst ∘ ⇑G.subtype)) (hG₂ : Function.Bijective (Prod.snd ∘ ⇑G.subtype)) : ∃ e, G = e.toAddMonoidHom.graph
• DFinsupp.ker_mapRangeAddMonoidHom 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommGroup (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i) : (DFinsupp.mapRange.addMonoidHom f).ker = AddSubgroup.comap DFinsupp.coeFnAddMonoidHom (AddSubgroup.pi Set.univ fun x => (f x).ker)
• DFinsupp.range_mapRangeAddMonoidHom 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommGroup (β₁ i)] [(i : ι) → AddCommGroup (β₂ i)] (f : (i : ι) → β₂ i →+ β₁ i) : (DFinsupp.mapRange.addMonoidHom f).range = AddSubgroup.comap DFinsupp.coeFnAddMonoidHom (AddSubgroup.pi Set.univ fun x => (f x).range)
• iSupIndep_of_dfinsuppSumAddHom_injective' 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommGroup N] (p : ι → AddSubgroup N) (h : Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)) : iSupIndep p
• iSupIndep_of_dfinsupp_sumAddHom_injective' 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommGroup N] (p : ι → AddSubgroup N) (h : Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)) : iSupIndep p
• independent_of_dfinsupp_sumAddHom_injective' 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommGroup N] (p : ι → AddSubgroup N) (h : Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)) : iSupIndep p
• Independent.dfinsupp_sumAddHom_injective 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommGroup N] {p : ι → AddSubgroup N} (h : iSupIndep p) : Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)
• iSupIndep.dfinsuppSumAddHom_injective 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommGroup N] {p : ι → AddSubgroup N} (h : iSupIndep p) : Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)
• iSupIndep.dfinsupp_sumAddHom_injective 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommGroup N] {p : ι → AddSubgroup N} (h : iSupIndep p) : Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)

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