Loogle!

Result

Found 162 declarations mentioning Subgroup.map.

• Subgroup.map_id 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] (K : Subgroup G) : Subgroup.map (MonoidHom.id G) K = K
• Subgroup.map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) : Subgroup N
• Subgroup.map_bot 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup.map f ⊥ = ⊥
• Subgroup.subgroupOf_map_subtype 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] (H K : Subgroup G) : Subgroup.map K.subtype (H.subgroupOf K) = H ⊓ K
• Subgroup.le_comap_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) : H ≤ Subgroup.comap f (Subgroup.map f H)
• Subgroup.map_comap_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup.map f (Subgroup.comap f H) ≤ H
• Subgroup.gc_map_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : GaloisConnection (Subgroup.map f) (Subgroup.comap f)
• Subgroup.map_subgroupOf_eq_of_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) : Subgroup.map K.subtype (H.subgroupOf K) = H
• Subgroup.map_iSup 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} (f : G →* N) (s : ι → Subgroup G) : Subgroup.map f (iSup s) = ⨆ i, Subgroup.map f (s i)
• Subgroup.map_one_eq_bot 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] (K : Subgroup G) {N : Type u_5} [Group N] : Subgroup.map 1 K = ⊥
• Subgroup.map_isCommutative 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') [IsMulCommutative ↥H] : IsMulCommutative ↥(Subgroup.map f H)
• Subgroup.map_isMulCommutative 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') [IsMulCommutative ↥H] : IsMulCommutative ↥(Subgroup.map f H)
• MonoidHom.map_closure 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (s : Set G) : Subgroup.map f (Subgroup.closure s) = Subgroup.closure (⇑f '' s)
• Subgroup.map_inf_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H K : Subgroup G) (f : G →* N) : Subgroup.map f (H ⊓ K) ≤ Subgroup.map f H ⊓ Subgroup.map f K
• Subgroup.map_top_of_surjective 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (h : Function.Surjective ⇑f) : Subgroup.map f ⊤ = ⊤
• Subgroup.map_mono 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K K' : Subgroup G} : K ≤ K' → Subgroup.map f K ≤ Subgroup.map f K'
• Subgroup.map_le_iff_le_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup G} {H : Subgroup N} : Subgroup.map f K ≤ H ↔ K ≤ Subgroup.comap f H
• Subgroup.map_sup 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H K : Subgroup G) (f : G →* N) : Subgroup.map f (H ⊔ K) = Subgroup.map f H ⊔ Subgroup.map f K
• Subgroup.coe_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (K : Subgroup G) : ↑(Subgroup.map f K) = ⇑f '' ↑K
• Subgroup.map_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] (K : Subgroup G) {N : Type u_5} [Group N] {P : Type u_6} [Group P] (g : N →* P) (f : G →* N) : Subgroup.map g (Subgroup.map f K) = Subgroup.map (g.comp f) K
• Subgroup.mem_map_of_mem 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {K : Subgroup G} {x : G} (hx : x ∈ K) : f x ∈ Subgroup.map f K
• Subgroup.comap_equiv_eq_map_symm' 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : N ≃* G) (K : Subgroup G) : Subgroup.comap f.toMonoidHom K = Subgroup.map f.symm.toMonoidHom K
• Subgroup.map_equiv_eq_comap_symm' 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G ≃* N) (K : Subgroup G) : Subgroup.map f.toMonoidHom K = Subgroup.comap f.symm.toMonoidHom K
• Subgroup.map_iInf 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} [Nonempty ι] (f : G →* N) (hf : Function.Injective ⇑f) (s : ι → Subgroup G) : Subgroup.map f (iInf s) = ⨅ i, Subgroup.map f (s i)
• Subgroup.map_inf 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H K : Subgroup G) (f : G →* N) (hf : Function.Injective ⇑f) : Subgroup.map f (H ⊓ K) = Subgroup.map f H ⊓ Subgroup.map f K
• Subgroup.map_inf_eq 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H K : Subgroup G) (f : G →* N) (hf : Function.Injective ⇑f) : Subgroup.map f (H ⊓ K) = Subgroup.map f H ⊓ Subgroup.map f K
• Subgroup.mem_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup G} {y : N} : y ∈ Subgroup.map f K ↔ ∃ x ∈ K, f x = y
• Subgroup.map_toSubmonoid 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (K : Subgroup G) : (Subgroup.map f K).toSubmonoid = Submonoid.map f K.toSubmonoid
• Subgroup.apply_coe_mem_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (K : Subgroup G) (x : ↥K) : f ↑x ∈ Subgroup.map f K
• Subgroup.equivMapOfInjective 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G →* N) (hf : Function.Injective ⇑f) : ↥H ≃* ↥(Subgroup.map f H)
• Subgroup.map.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) : Subgroup.map f H = { carrier := ⇑f '' ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
• Subgroup.mem_map_iff_mem 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) {K : Subgroup G} {x : G} : f x ∈ Subgroup.map f K ↔ x ∈ K
• Subgroup.mem_map_equiv 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G ≃* N} {K : Subgroup G} {x : N} : x ∈ Subgroup.map f.toMonoidHom K ↔ f.symm x ∈ K
• MulEquiv.coe_mapSubgroup 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {H : Type u_5} [Group H] (e : G ≃* H) : ⇑e.mapSubgroup = Subgroup.map e.toMonoidHom
• MonoidHom.subgroupMap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) : ↥H →* ↥(Subgroup.map f H)
• Subgroup.map_eq_comap_of_inverse 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (hl : Function.LeftInverse ⇑g ⇑f) (hr : Function.RightInverse ⇑g ⇑f) (H : Subgroup G) : Subgroup.map f H = Subgroup.comap g H
• MonoidHom.subgroupMap.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) : f.subgroupMap H = f.submonoidMap H.toSubmonoid
• Subgroup.equivMapOfInjective.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G →* N) (hf : Function.Injective ⇑f) : H.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_mul' := ⋯ }
• MulEquiv.mapSubgroup_apply 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {H : Type u_6} [Group H] (f : G ≃* H) (H✝ : Subgroup G) : f.mapSubgroup H✝ = Subgroup.map (↑f) H✝
• MulEquiv.mapSubgroup_symm_apply 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {H : Type u_6} [Group H] (f : G ≃* H) (H✝ : Subgroup H) : (RelIso.symm f.mapSubgroup) H✝ = Subgroup.map (↑f.symm) H✝
• MulEquiv.mapSubgroup.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {H : Type u_6} [Group H] (f : G ≃* H) : f.mapSubgroup = { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
• Subgroup.comap_equiv_eq_map_symm 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : N ≃* G) (K : Subgroup G) : Subgroup.comap (↑f) K = Subgroup.map (↑f.symm) K
• Subgroup.map_equiv_eq_comap_symm 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G ≃* N) (K : Subgroup G) : Subgroup.map (↑f) K = Subgroup.comap (↑f.symm) K
• Subgroup.map_symm_eq_iff_map_eq 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] (K : Subgroup G) {N : Type u_5} [Group N] {H : Subgroup N} {e : G ≃* N} : Subgroup.map (↑e.symm) H = K ↔ Subgroup.map (↑e) K = H
• MulEquiv.subgroupMap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) : ↥H ≃* ↥(Subgroup.map (↑e) H)
• MulEquiv.subgroupMap.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) : e.subgroupMap H = e.submonoidMap H.toSubmonoid
• Subgroup.coe_equivMapOfInjective_apply 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G →* N) (hf : Function.Injective ⇑f) (h : ↥H) : ↑((H.equivMapOfInjective f hf) h) = f ↑h
• MonoidHom.subgroupMap_surjective 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) : Function.Surjective ⇑(f.subgroupMap H)
• Subgroup.equivMapOfInjective_coe_mulEquiv 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (e : G ≃* G') : H.equivMapOfInjective ↑e ⋯ = e.subgroupMap H
• MonoidHom.subgroupMap_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) (x : ↥H.toSubmonoid) : ↑((f.subgroupMap H) x) = f ↑x
• MulEquiv.coe_subgroupMap_apply 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) (g : ↥H) : ↑((e.subgroupMap H) g) = e ↑g
• MulEquiv.subgroupMap_symm_apply 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) (g : ↥(Subgroup.map (↑e) H)) : (e.subgroupMap H).symm g = ⟨e.symm ↑g, ⋯⟩
• MonoidHom.range_eq_map 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : f.range = Subgroup.map f ⊤
• Subgroup.map_comap_eq 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup.map f (Subgroup.comap f H) = f.range ⊓ H
• Subgroup.map_le_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) : Subgroup.map f H ≤ f.range
• Subgroup.map_comap_eq_self 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup N} (h : H ≤ f.range) : Subgroup.map f (Subgroup.comap f H) = H
• Subgroup.comap_map_eq 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) : Subgroup.comap f (Subgroup.map f H) = H ⊔ f.ker
• Subgroup.map_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Injective ⇑f) : Function.Injective (Subgroup.map f)
• Subgroup.comap_map_eq_self 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} (h : f.ker ≤ H) : Subgroup.comap f (Subgroup.map f H) = H
• Subgroup.map_eq_bot_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : G →* N} : Subgroup.map f H = ⊥ ↔ H ≤ f.ker
• Subgroup.map_subtype_le 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {H : Subgroup G} (K : Subgroup ↥H) : Subgroup.map H.subtype K ≤ H
• Subgroup.comap_map_eq_self_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Injective ⇑f) (H : Subgroup G) : Subgroup.comap f (Subgroup.map f H) = H
• Subgroup.map_comap_eq_self_of_surjective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Surjective ⇑f) (H : Subgroup N) : Subgroup.map f (Subgroup.comap f H) = H
• MonoidHom.map_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} {P : Type u_6} [Group N] [Group P] (g : N →* P) (f : G →* N) : Subgroup.map g f.range = (g.comp f).range
• MonoidHom.range_comp 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} {P : Type u_6} [Group N] [Group P] (g : N →* P) (f : G →* N) : (g.comp f).range = Subgroup.map g f.range
• MonoidHom.range.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : f.range = (Subgroup.map f ⊤).copy (Set.range ⇑f) ⋯
• Subgroup.map_eq_bot_iff_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : G →* N} (hf : Function.Injective ⇑f) : Subgroup.map f H = ⊥ ↔ H = ⊥
• MonoidHom.restrict_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) (f : G →* N) : (f.restrict K).range = Subgroup.map f K
• Subgroup.map_eq_range_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} : Subgroup.map f H = f.range ↔ Codisjoint H f.ker
• Subgroup.map_eq_map_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H K : Subgroup G} : Subgroup.map f H = Subgroup.map f K ↔ H ⊔ f.ker = K ⊔ f.ker
• Subgroup.map_le_map_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H K : Subgroup G} : Subgroup.map f H ≤ Subgroup.map f K ↔ H ≤ K ⊔ f.ker
• Subgroup.map_injective_of_ker_le 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {H K : Subgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K) (hf : Subgroup.map f H = Subgroup.map f K) : H = K
• Subgroup.map_le_map_iff_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) {H K : Subgroup G} : Subgroup.map f H ≤ Subgroup.map f K ↔ H ≤ K
• Subgroup.map_lt_map_iff_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) {H K : Subgroup G} : Subgroup.map f H < Subgroup.map f K ↔ H < K
• Subgroup.map_le_map_iff' 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H K : Subgroup G} : Subgroup.map f H ≤ Subgroup.map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker
• Subgroup.ker_subgroupMap 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G →* N) : (f.subgroupMap H).ker = f.ker.subgroupOf H
• Subgroup.map_subtype_le_map_subtype 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {G' : Subgroup G} {H K : Subgroup ↥G'} : Subgroup.map G'.subtype H ≤ Subgroup.map G'.subtype K ↔ H ≤ K
• Subgroup.map_subtype_lt_map_subtype 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {G' : Subgroup G} {H K : Subgroup ↥G'} : Subgroup.map G'.subtype H < Subgroup.map G'.subtype K ↔ H < K
• 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)
• Subgroup.characteristic_iff_map_eq 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom H = H
• Subgroup.le_normalizer_map 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {H : Subgroup G} {N : Type u_5} [Group N] (f : G →* N) : Subgroup.map f H.normalizer ≤ (Subgroup.map f H).normalizer
• Subgroup.characteristic_iff_le_map 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ Subgroup.map ϕ.toMonoidHom H
• Subgroup.characteristic_iff_map_le 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom H ≤ H
• Subgroup.Normal.map 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} (h : H.Normal) (f : G →* N) (hf : Function.Surjective ⇑f) : (Subgroup.map f H).Normal
• Subgroup.Normal.of_map_injective 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_6} {H : Type u_7} [Group G] [Group H] {φ : G →* H} (hφ : Function.Injective ⇑φ) {L : Subgroup G} (n : (Subgroup.map φ L).Normal) : L.Normal
• Subgroup.Normal.of_map_subtype 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {K : Subgroup G} {L : Subgroup ↥K} (n : (Subgroup.map K.subtype L).Normal) : L.Normal
• Subgroup.map_equiv_normalizer_eq 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G ≃* N) : Subgroup.map f.toMonoidHom H.normalizer = (Subgroup.map f.toMonoidHom H).normalizer
• Subgroup.map_normalizer_eq_of_bijective 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : G →* N} (hf : Function.Bijective ⇑f) : Subgroup.map f H.normalizer = (Subgroup.map f H).normalizer
• Subgroup.map_normalClosure 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] (s : Set G) (f : G →* N) (hf : Function.Surjective ⇑f) : Subgroup.map f (Subgroup.normalClosure s) = Subgroup.normalClosure (⇑f '' s)
• Subgroup.le_pi_iff 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] {I : Set η} {H : (i : η) → Subgroup (f i)} {J : Subgroup ((i : η) → f i)} : J ≤ Subgroup.pi I H ↔ ∀ i ∈ I, Subgroup.map (Pi.evalMonoidHom f i) J ≤ H i
• Subgroup.le_prod_iff 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} : J ≤ H.prod K ↔ Subgroup.map (MonoidHom.fst G N) J ≤ H ∧ Subgroup.map (MonoidHom.snd G N) J ≤ K
• Subgroup.prod_le_iff 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} : H.prod K ≤ J ↔ Subgroup.map (MonoidHom.inl G N) H ≤ J ∧ Subgroup.map (MonoidHom.inr G N) K ≤ J
• MonoidHom.map_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
  {G : Type u_1} [Group G] {N : Type u_3} [Group N] (f : G →* N) (x : G) : Subgroup.map f (Subgroup.zpowers x) = Subgroup.zpowers (f x)
• Subgroup.map_centralizer_le_centralizer_image 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (s : Set G) (f : G →* G') : Subgroup.map f (Subgroup.centralizer s) ≤ Subgroup.centralizer (⇑f '' s)
• ConjAct.normal_of_characteristic_of_normal 📋 Mathlib.GroupTheory.GroupAction.ConjAct
  {G : Type u_3} [Group G] {H : Subgroup G} [hH : H.Normal] {K : Subgroup ↥H} [h : K.Characteristic] : (Subgroup.map H.subtype K).Normal
• Subgroup.pointwise_smul_def 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] {a : α} (S : Subgroup G) : a • S = Subgroup.map ((MulDistribMulAction.toMonoidEnd α G) a) S
• Subgroup.card_map_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Finite
  {G : Type u_1} [Group G] {H : Type u_3} [Group H] {K : Subgroup G} {f : G →* H} (hf : Function.Injective ⇑f) : Nat.card ↥(Subgroup.map f K) = Nat.card ↥K
• Subgroup.pi_le_iff 📋 Mathlib.Algebra.Group.Subgroup.Finite
  {η : Type u_3} {f : η → Type u_4} [(i : η) → Group (f i)] [DecidableEq η] [Finite η] {H : (i : η) → Subgroup (f i)} {J : Subgroup ((i : η) → f i)} : Subgroup.pi Set.univ H ≤ J ↔ ∀ (i : η), Subgroup.map (MonoidHom.mulSingle f i) (H i) ≤ J
• Subgroup.card_subtype 📋 Mathlib.Algebra.Group.Subgroup.Finite
  {G : Type u_1} [Group G] (K : Subgroup G) (L : Subgroup ↥K) : Nat.card ↥(Subgroup.map K.subtype L) = Nat.card ↥L
• QuotientGroup.map_mk'_self 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : Subgroup.map (QuotientGroup.mk' N) N = ⊥
• QuotientGroup.ker_lift 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] (φ : G →* M) (HN : N ≤ φ.ker) : (QuotientGroup.lift N φ HN).ker = Subgroup.map (QuotientGroup.mk' N) φ.ker
• QuotientGroup.ker_map 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) : (QuotientGroup.map N M f h).ker = Subgroup.map (QuotientGroup.mk' N) (Subgroup.comap f M)
• QuotientGroup.congr 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') : G ⧸ G' ≃* H ⧸ H'
• QuotientGroup.congr_refl 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [Group G] (G' : Subgroup G) [G'.Normal] (he : Subgroup.map (↑(MulEquiv.refl G)) G' = G' := ⋯) : QuotientGroup.congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')
• QuotientGroup.congr_mk 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) : (QuotientGroup.congr G' H' e he) ↑x = ↑(e x)
• QuotientGroup.congr_apply 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) : (QuotientGroup.congr G' H' e he) ↑x = (QuotientGroup.mk' H') (e x)
• QuotientGroup.congr_symm 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') : (QuotientGroup.congr G' H' e he).symm = QuotientGroup.congr H' G' e.symm ⋯
• QuotientGroup.congr_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) : (QuotientGroup.congr G' H' e he) ((QuotientGroup.mk' G') x) = (QuotientGroup.mk' H') (e x)
• QuotientGroup.congr.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') : QuotientGroup.congr G' H' e he = { toFun := ⇑(QuotientGroup.map G' H' ↑e ⋯), invFun := ⇑(QuotientGroup.map H' G' ↑e.symm ⋯), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
• QuotientGroup.map_normal 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] : (Subgroup.map (QuotientGroup.mk' N) M).Normal
• QuotientGroup.comap_map_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [Group G] (N H : Subgroup G) [N.Normal] : Subgroup.comap (QuotientGroup.mk' N) (Subgroup.map (QuotientGroup.mk' N) H) = N ⊔ H
• QuotientGroup.strictMono_comap_prod_map 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : StrictMono fun H => (Subgroup.comap N.subtype H, Subgroup.map (QuotientGroup.mk' N) H)
• QuotientGroup.quotientQuotientEquivQuotientAux 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M →* G ⧸ M
• QuotientGroup.quotientQuotientEquivQuotient 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M ≃* G ⧸ M
• QuotientGroup.quotientQuotientEquivQuotientAux.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) : QuotientGroup.quotientQuotientEquivQuotientAux N M h = QuotientGroup.lift (Subgroup.map (QuotientGroup.mk' N) M) (QuotientGroup.map N M (MonoidHom.id G) h) ⋯
• QuotientGroup.comapMk'OrderIso.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [Group G] (N : Subgroup G) [hn : N.Normal] : QuotientGroup.comapMk'OrderIso N = { toFun := fun H' => ⟨Subgroup.comap (QuotientGroup.mk' N) H', ⋯⟩, invFun := fun H => Subgroup.map (QuotientGroup.mk' N) ↑H, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
• QuotientGroup.quotientQuotientEquivQuotient.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) : QuotientGroup.quotientQuotientEquivQuotient N M h = (QuotientGroup.quotientQuotientEquivQuotientAux N M h).toMulEquiv (QuotientGroup.map M (Subgroup.map (QuotientGroup.mk' N) M) (QuotientGroup.mk' N) ⋯) ⋯ ⋯
• QuotientGroup.quotientQuotientEquivQuotientAux_mk_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) (x : G) : (QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x
• QuotientGroup.quotientQuotientEquivQuotientAux_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) (x : G ⧸ N) : (QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑x = (QuotientGroup.map N M (MonoidHom.id G) h) x
• Subgroup.map_commutator 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H₁ H₂ : Subgroup G) (f : G →* G') : Subgroup.map f ⁅H₁, H₂⁆ = ⁅Subgroup.map f H₁, Subgroup.map f H₂⁆
• Subgroup.commutator_le_map_commutator 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {H₁ H₂ : Subgroup G} {f : G →* G'} {K₁ K₂ : Subgroup G'} (h₁ : K₁ ≤ Subgroup.map f H₁) (h₂ : K₂ ≤ Subgroup.map f H₂) : ⁅K₁, K₂⁆ ≤ Subgroup.map f ⁅H₁, H₂⁆
• MulAction.stabilizer_smul_eq_stabilizer_map_conj 📋 Mathlib.GroupTheory.GroupAction.Basic
  {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (g : G) (a : α) : MulAction.stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (MulAction.stabilizer G a)
• MulAction.stabilizerEquivStabilizerOfOrbitRel.eq_1 📋 Mathlib.GroupTheory.GroupAction.Basic
  {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {a b : α} (h : (MulAction.orbitRel G α) a b) : MulAction.stabilizerEquivStabilizerOfOrbitRel h = (MulEquiv.subgroupCongr ⋯).trans (MulEquiv.subgroupMap (MulAut.conj (Classical.choose h)) (MulAction.stabilizer G b)).symm
• Subgroup.relindex_comap 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G' →* G) (K : Subgroup G') : (Subgroup.comap f H).relindex K = H.relindex (Subgroup.map f K)
• Subgroup.relindex_ker 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (K : Subgroup G) (f : G →* G') : f.ker.relindex K = Nat.card ↥(Subgroup.map f K)
• Subgroup.card_map_dvd 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') : Nat.card ↥(Subgroup.map f H) ∣ Nat.card ↥H
• Subgroup.dvd_index_map 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G →* G'} (hf : f.ker ≤ H) : H.index ∣ (Subgroup.map f H).index
• Subgroup.index_map_of_bijective 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Bijective ⇑f) (H : Subgroup G) : (Subgroup.map f H).index = H.index
• Subgroup.index_map_dvd 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G →* G'} (hf : Function.Surjective ⇑f) : (Subgroup.map f H).index ∣ H.index
• Subgroup.index_map 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') : (Subgroup.map f H).index = (H ⊔ f.ker).index * f.range.index
• Subgroup.index_map_subtype 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} [Group G] {H : Subgroup G} (K : Subgroup ↥H) : (Subgroup.map H.subtype K).index = K.index * H.index
• Subgroup.index_map_of_injective 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G →* G'} (hf : Function.Injective ⇑f) : (Subgroup.map f H).index = H.index * f.range.index
• Subgroup.index_map_eq 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G →* G'} (hf1 : Function.Surjective ⇑f) (hf2 : f.ker ≤ H) : (Subgroup.map f H).index = H.index
• map_commutator_eq 📋 Mathlib.GroupTheory.Abelianization
  (G : Type u) [Group G] {H : Type u_1} [Group H] (f : G →* H) : Subgroup.map f (commutator G) = ⁅f.range, f.range⁆
• Subgroup.map_subtype_commutator 📋 Mathlib.GroupTheory.Abelianization
  {G : Type u} [Group G] (H : Subgroup G) : Subgroup.map H.subtype (commutator ↥H) = ⁅H, H⁆
• DenseRange.topologicalClosure_map_subgroup 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type w} {H : Type x} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {f : G →* H} (hf : Continuous ⇑f) (hf' : DenseRange ⇑f) {s : Subgroup G} (hs : s.topologicalClosure = ⊤) : (Subgroup.map f s).topologicalClosure = ⊤
• IsPGroup.map 📋 Mathlib.GroupTheory.PGroup
  {p : ℕ} {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsPGroup p ↥H) {K : Type u_2} [Group K] (ϕ : G →* K) : IsPGroup p ↥(Subgroup.map ϕ H)
• Sylow.coe_mapSurjective 📋 Mathlib.GroupTheory.Sylow
  {p : ℕ} {G : Type u_1} [Group G] [Finite G] {G' : Type u_2} [Group G'] {f : G →* G'} (hf : Function.Surjective ⇑f) [Fact (Nat.Prime p)] (P : Sylow p G) : ↑(Sylow.mapSurjective hf P) = Subgroup.map f ↑P
• Sylow.normalizer_sup_eq_top 📋 Mathlib.GroupTheory.Sylow
  {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] {N : Subgroup G} [N.Normal] [Finite (Sylow p ↥N)] (P : Sylow p ↥N) : (Subgroup.map N.subtype ↑P).normalizer ⊔ N = ⊤
• map_rootsOfUnity 📋 Mathlib.RingTheory.RootsOfUnity.Basic
  {M : Type u_1} {N : Type u_2} [CommMonoid M] [CommMonoid N] (f : Mˣ →* Nˣ) (k : ℕ) : Subgroup.map f (rootsOfUnity k M) ≤ rootsOfUnity k N
• Subgroup.isCoatom_map 📋 Mathlib.Algebra.Group.Subgroup.Order
  {G : Type u_1} [Group G] (H : Subgroup G) (f : G ≃* ↥H) {K : Subgroup G} : IsCoatom (Subgroup.map (↑f) K) ↔ IsCoatom K
• MulAction.map_stabilizer_le 📋 Mathlib.Algebra.Pointwise.Stabilizer
  {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (s : Set G) : Subgroup.map f (MulAction.stabilizer G s) ≤ MulAction.stabilizer H (⇑f '' s)
• map_derivedSeries_le_derivedSeries 📋 Mathlib.GroupTheory.Solvable
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (n : ℕ) : Subgroup.map f (derivedSeries G n) ≤ derivedSeries G' n
• map_derivedSeries_eq 📋 Mathlib.GroupTheory.Solvable
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Surjective ⇑f) (n : ℕ) : Subgroup.map f (derivedSeries G n) = derivedSeries G' n
• derivedSeries_le_map_derivedSeries 📋 Mathlib.GroupTheory.Solvable
  {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Surjective ⇑f) (n : ℕ) : derivedSeries G' n ≤ Subgroup.map f (derivedSeries G n)
• IsPrimitiveRoot.map_rootsOfUnity 📋 Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
  {R : Type u_4} [CommRing R] [IsDomain R] {S : Type u_7} {F : Type u_8} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {ζ : R} {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) {f : F} (hf : Function.Injective ⇑f) : Subgroup.map (Units.map ↑f) (rootsOfUnity n R) = rootsOfUnity n S
• InfiniteGalois.restrict_fixedField 📋 Mathlib.FieldTheory.Galois.Infinite
  {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (H : Subgroup (K ≃ₐ[k] K)) (L : IntermediateField k K) [Normal k ↥L] : IntermediateField.fixedField H ⊓ L = IntermediateField.lift (IntermediateField.fixedField (Subgroup.map (AlgEquiv.restrictNormalHom ↥L) H))
• lowerCentralSeries.map 📋 Mathlib.GroupTheory.Nilpotent
  {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (n : ℕ) : Subgroup.map f (lowerCentralSeries G n) ≤ lowerCentralSeries H n
• lowerCentralSeries_map_subtype_le 📋 Mathlib.GroupTheory.Nilpotent
  {G : Type u_1} [Group G] (H : Subgroup G) (n : ℕ) : Subgroup.map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n
• upperCentralSeries.map 📋 Mathlib.GroupTheory.Nilpotent
  {G : Type u_1} [Group G] {H : Type u_2} [Group H] {f : G →* H} (h : Function.Surjective ⇑f) (n : ℕ) : Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n
• Subgroup.goursatFst.eq_1 📋 Mathlib.GroupTheory.Goursat
  {G : Type u_1} {H : Type u_2} [Group G] [Group H] (I : Subgroup (G × H)) : I.goursatFst = Subgroup.map ((MonoidHom.fst G H).comp I.subtype) ((MonoidHom.snd G H).comp I.subtype).ker
• Subgroup.goursatSnd.eq_1 📋 Mathlib.GroupTheory.Goursat
  {G : Type u_1} {H : Type u_2} [Group G] [Group H] (I : Subgroup (G × H)) : I.goursatSnd = Subgroup.map ((MonoidHom.snd G H).comp I.subtype) ((MonoidHom.fst G H).comp I.subtype).ker
• Subgroup.goursat 📋 Mathlib.GroupTheory.Goursat
  {G : Type u_1} {H : Type u_2} [Group G] [Group H] {I : Subgroup (G × H)} : ∃ G' H' M N, ∃ (x : M.Normal) (x_1 : N.Normal), ∃ e, I = Subgroup.map (G'.subtype.prodMap H'.subtype) (Subgroup.comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)
• MulAction.IsBlock.of_subgroup_of_conjugate 📋 Mathlib.GroupTheory.GroupAction.Blocks
  {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} {H : Subgroup G} (hB : MulAction.IsBlock (↥H) B) (g : G) : MulAction.IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)) (g • B)
• Equiv.Perm.OnCycleFactors.kerParam_range_eq 📋 Mathlib.GroupTheory.Perm.Centralizer
  {α : Type u_1} [DecidableEq α] [Fintype α] {g : Equiv.Perm α} : (Equiv.Perm.OnCycleFactors.kerParam g).range = Subgroup.map (Subgroup.centralizer {g}).subtype (Equiv.Perm.OnCycleFactors.toPermHom g).ker
• CongruenceSubgroup.Gamma1.eq_1 📋 Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
  (N : ℕ) : CongruenceSubgroup.Gamma1 N = Subgroup.map ((CongruenceSubgroup.Gamma0 N).subtype.comp (CongruenceSubgroup.Gamma1' N).subtype) ⊤
• CongruenceSubgroup.conjGLPos.eq_1 📋 Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
  (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (g : ↥(Matrix.GLPos (Fin 2) ℝ)) : CongruenceSubgroup.conjGLPos Γ g = Subgroup.comap ModularGroup.coeHom (ConjAct.toConjAct g⁻¹ • Subgroup.map ModularGroup.coeHom Γ)
• CuspForm.translate 📋 Mathlib.NumberTheory.ModularForms.Basic
  {k : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) [CuspFormClass F Γ k] : CuspForm (Subgroup.map (↑(MulAut.conj g⁻¹)) Γ) k
• ModularForm.translate 📋 Mathlib.NumberTheory.ModularForms.Basic
  {k : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) [ModularFormClass F Γ k] : ModularForm (Subgroup.map (↑(MulAut.conj g⁻¹)) Γ) k
• CuspForm.coe_translate 📋 Mathlib.NumberTheory.ModularForms.Basic
  {k : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) [CuspFormClass F Γ k] : ⇑(CuspForm.translate f g) = SlashAction.map ℂ k g ⇑f
• ModularForm.coe_translate 📋 Mathlib.NumberTheory.ModularForms.Basic
  {k : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) [ModularFormClass F Γ k] : ⇑(ModularForm.translate f g) = SlashAction.map ℂ k g ⇑f

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 40fea08