Loogle!

Result

Found 241 declarations mentioning AddSubgroup.Normal. Of these, only the first 200 are shown.

• AddSubgroup.Normal 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {A : Type u_2} [AddGroup A] (H : AddSubgroup A) : Prop
• AddSubgroup.normal_of_isAddCommutative 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] [IsAddCommutative G] (H : AddSubgroup G) : H.Normal
• AddSubgroup.Normal.mem_comm 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (nH : H.Normal) {a b : G} (h : a + b ∈ H) : b + a ∈ H
• AddSubgroup.Normal.mem_comm_iff 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (nH : H.Normal) {a b : G} : a + b ∈ H ↔ b + a ∈ H
• AddSubgroup.Normal.conj_mem 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {A : Type u_2} [AddGroup A] {H : AddSubgroup A} (self : H.Normal) (n : A) : n ∈ H → ∀ (g : A), g + n + -g ∈ H
• AddSubgroup.Normal.mk 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {A : Type u_2} [AddGroup A] {H : AddSubgroup A} (conj_mem : ∀ n ∈ H, ∀ (g : A), g + n + -g ∈ H) : H.Normal
• AddSubgroup.Normal.addConj_mem' 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (nH : H.Normal) (n : G) (hn : n ∈ H) (g : G) : -g + n + g ∈ H
• AddSubgroup.mem_sup_of_normal_left 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [AddGroup G] {s t : AddSubgroup G} [hs : s.Normal] {x : G} : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x
• AddSubgroup.mem_sup_of_normal_right 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [AddGroup G] {s t : AddSubgroup G} [ht : t.Normal] {x : G} : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x
• AddMonoidHom.normal_ker 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {M : Type u_6} [AddZeroClass M] (f : G →+ M) : f.ker.Normal
• AddSubgroup.normalClosure_normal 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {s : Set G} : (AddSubgroup.normalClosure s).Normal
• AddSubgroup.normalCore_normal 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.normalCore.Normal
• AddSubgroup.normal_bot 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] : ⊥.Normal
• AddSubgroup.normal_top 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] : ⊤.Normal
• AddSubgroup.normal_of_characteristic 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {A : Type u_3} [AddGroup A] (H : AddSubgroup A) [h : H.Characteristic] : H.Normal
• AddSubgroup.normalCore_eq_self 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.Normal] : H.normalCore = H
• AddSubgroup.normal_iInf_normal 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {ι : Sort u_5} {a : ι → AddSubgroup G} (norm : ∀ (i : ι), (a i).Normal) : (iInf a).Normal
• AddSubgroup.normalClosure_eq_self 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.Normal] : AddSubgroup.normalClosure ↑H = H
• AddSubgroup.normal_inf_normal 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊓ K).Normal
• AddSubgroup.normalizer_eq_top 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [h : H.Normal] : AddSubgroup.normalizer ↑H = ⊤
• AddSubgroup.normalizer_eq_top_iff 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : AddSubgroup.normalizer ↑H = ⊤ ↔ H.Normal
• AddSubgroup.prod_normal 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_4} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) [hH : H.Normal] [hK : K.Normal] : (H.prod K).Normal
• AddSubgroup.subset_normalizer_of_normal 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} [hH : H.Normal] : S ⊆ ↑(AddSubgroup.normalizer ↑H)
• AddSubgroup.le_normalizer_of_normal 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [H.Normal] : K ≤ AddSubgroup.normalizer ↑H
• AddSubgroup.normal_addSubgroupOf 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H N : AddSubgroup G} [N.Normal] : (N.addSubgroupOf H).Normal
• AddSubgroup.Normal.addSubgroupOf 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : H.Normal) (K : AddSubgroup G) : (H.addSubgroupOf K).Normal
• AddSubgroup.normal_comap 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_4} [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_4} [AddGroup N] {H : AddSubgroup N} (hH : H.Normal) (f : G →+ N) : (AddSubgroup.comap f H).Normal
• AddGroup.addConjugatesOfSet_subset 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {s : Set G} {N : AddSubgroup G} [N.Normal] (h : s ⊆ ↑N) : AddGroup.addConjugatesOfSet s ⊆ ↑N
• AddSubgroup.normal_addSubgroupOf_closure_normalizer 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] (s : Set G) : ((AddSubgroup.closure s).addSubgroupOf (AddSubgroup.normalizer s)).Normal
• AddSubgroup.normalClosure_le_normal 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {s : Set G} {N : AddSubgroup G} [N.Normal] (h : s ⊆ ↑N) : AddSubgroup.normalClosure s ≤ N
• AddGroup.addConjugates_subset_normal 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : AddSubgroup G} [tn : N.Normal] {a : G} (h : a ∈ N) : addConjugatesOf a ⊆ ↑N
• AddSubgroup.normalClosure_subset_iff 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {s : Set G} {N : AddSubgroup G} [N.Normal] : s ⊆ ↑N ↔ AddSubgroup.normalClosure s ≤ N
• AddSubgroup.normal_le_normalCore 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H N : AddSubgroup G} [hN : N.Normal] : N ≤ H.normalCore ↔ N ≤ H
• AddSubgroup.maximal_normal_addSubgroupOf_normalizer 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : Maximal (fun x => (H.addSubgroupOf x).Normal) (AddSubgroup.normalizer ↑H)
• AddSubgroup.normal_addSubgroupOf_of_le_normalizer 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H N : AddSubgroup G} (hLE : H ≤ AddSubgroup.normalizer ↑N) : (N.addSubgroupOf H).Normal
• AddSubgroup.normal_in_normalizer 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : (H.addSubgroupOf (AddSubgroup.normalizer ↑H)).Normal
• AddSubgroup.normal_addSubgroupOf_iff_le_normalizer_inf 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : (H.addSubgroupOf K).Normal ↔ K ≤ AddSubgroup.normalizer ↑(H ⊓ K)
• AddSubgroup.normalClosure_eq_iInf 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {s : Set G} : AddSubgroup.normalClosure s = ⨅ N, ⨅ (_ : N.Normal), ⨅ (_ : s ⊆ ↑N), N
• AddSubgroup.le_normalizer_of_normal_addSubgroupOf 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [hK : (H.addSubgroupOf K).Normal] (HK : H ≤ K) : K ≤ AddSubgroup.normalizer ↑H
• AddSubgroup.normal_addSubgroupOf_iff_le_normalizer 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : (H.addSubgroupOf K).Normal ↔ K ≤ AddSubgroup.normalizer ↑H
• AddSubgroup.Normal.map 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_4} [AddGroup N] {H : AddSubgroup G} (h : H.Normal) (f : G →+ N) (hf : Function.Surjective ⇑f) : (AddSubgroup.map f H).Normal
• AddSubgroup.addCommute_of_normal_of_disjoint 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) (hH₁ : H₁.Normal) (hH₂ : H₂.Normal) (hdis : Disjoint H₁ H₂) (x y : G) (hx : x ∈ H₁) (hy : y ∈ H₂) : AddCommute x y
• AddSubgroup.inf_addSubgroupOf_inf_normal_of_left 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {A' A : AddSubgroup G} (B : AddSubgroup G) [hN : (A'.addSubgroupOf A).Normal] : ((A' ⊓ B).addSubgroupOf (A ⊓ B)).Normal
• AddSubgroup.inf_addSubgroupOf_inf_normal_of_right 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] (A B' B : AddSubgroup G) [hN : (B'.addSubgroupOf B).Normal] : ((A ⊓ B').addSubgroupOf (A ⊓ B)).Normal
• AddSubgroup.normalCore_eq_iSup 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.normalCore = ⨆ N, ⨆ (_ : N.Normal), ⨆ (_ : N ≤ H), N
• AddSubgroup.normal_addSubgroupOf_sup_of_le_normalizer 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H N : AddSubgroup G} (hLE : H ≤ AddSubgroup.normalizer ↑N) : (N.addSubgroupOf (H ⊔ N)).Normal
• AddSubgroup.SubgroupNormal.mem_comm 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (hK : H ≤ K) [hN : (H.addSubgroupOf K).Normal] {a b : G} (hb : b ∈ K) (h : a + b ∈ H) : b + a ∈ H
• AddSubgroup.normal_addSubgroupOf_iff 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (hHK : H ≤ K) : (H.addSubgroupOf K).Normal ↔ ∀ (h k : G), h ∈ H → k ∈ K → k + h + -k ∈ H
• AddSubgroup.prod_addSubgroupOf_prod_normal 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_4} [AddGroup N] {H₁ K₁ : AddSubgroup G} {H₂ K₂ : AddSubgroup N} [h₁ : (H₁.addSubgroupOf K₁).Normal] [h₂ : (H₂.addSubgroupOf K₂).Normal] : ((H₁.prod H₂).addSubgroupOf (K₁.prod K₂)).Normal
• AddSubgroup.Normal.map_addConj_eq 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.Normal] (g : G) : AddSubgroup.map (↑(AddAut.addConj g)) H = H
• AddSubgroup.normal_iff_map_addConj_eq 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Normal ↔ ∀ (g : G), AddSubgroup.map (↑(AddAut.addConj g)) H = H
• AddSubgroup.Normal.of_op 📋 Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
  {G : Type u_2} [AddGroup G] {H : AddSubgroup G} : H.op.Normal → H.Normal
• AddSubgroup.Normal.op 📋 Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
  {G : Type u_2} [AddGroup G] {H : AddSubgroup G} : H.Normal → H.op.Normal
• AddSubgroup.op.instNormal 📋 Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
  {G : Type u_2} [AddGroup G] {H : AddSubgroup G} [H.Normal] : H.op.Normal
• AddSubgroup.normal_op 📋 Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
  {G : Type u_2} [AddGroup G] {H : AddSubgroup G} : H.op.Normal ↔ H.Normal
• AddSubgroup.Normal.of_unop 📋 Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
  {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} : H.unop.Normal → H.Normal
• AddSubgroup.Normal.unop 📋 Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
  {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} : H.Normal → H.unop.Normal
• AddSubgroup.unop.instNormal 📋 Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
  {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} [H.Normal] : H.unop.Normal
• AddSubgroup.normal_unop 📋 Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
  {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} : H.unop.Normal ↔ H.Normal
• AddSubgroup.instNormalCenter 📋 Mathlib.GroupTheory.Subgroup.Center
  {G : Type u_1} [AddGroup G] : (AddSubgroup.center G).Normal
• AddSubgroup.normal_of_le_center 📋 Mathlib.GroupTheory.Subgroup.Center
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : H ≤ AddSubgroup.center G) : H.Normal
• AddSubgroup.normal_centralizer 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [H.Normal] : (AddSubgroup.centralizer ↑H).Normal
• AddSubgroup.normal_addSubgroupOf_centralizer_normalizer 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} [AddGroup G] (s : Set G) : ((AddSubgroup.centralizer s).addSubgroupOf (AddSubgroup.normalizer s)).Normal
• AddSubgroup.iSup_normal 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [AddGroup G] {ι : Sort u_5} (H : ι → AddSubgroup G) [∀ (i : ι), (H i).Normal] : (⨆ i, H i).Normal
• AddSubgroup.sup_normal 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [AddGroup G] (H K : AddSubgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊔ K).Normal
• AddSubgroup.sSup_normal 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [AddGroup G] (Hs : Set (AddSubgroup G)) (h : ∀ H ∈ Hs, H.Normal) : (sSup Hs).Normal
• AddSubgroup.normalizer_le_normalizer_sup_normal 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [AddGroup G] {H K : AddSubgroup G} [hK : K.Normal] : AddSubgroup.normalizer ↑H ≤ AddSubgroup.normalizer ↑(H ⊔ K)
• AddSubgroup.set_add_normal_comm 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [AddGroup G] (S : Set G) (N : AddSubgroup G) [hN : N.Normal] : S + ↑N = ↑N + S
• AddSubgroup.add_normal 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [AddGroup G] (H N : AddSubgroup G) [hN : N.Normal] : ↑(H ⊔ N) = ↑H + ↑N
• AddSubgroup.normal_add 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [AddGroup G] (N H : AddSubgroup G) [N.Normal] : ↑(N ⊔ H) = ↑N + ↑H
• AddSubgroup.biSup_normal 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [AddGroup G] {ι : Type u_5} (s : Set ι) (H : ι → AddSubgroup G) (h : ∀ i ∈ s, (H i).Normal) : (⨆ i ∈ s, H i).Normal
• QuotientAddGroup.Quotient.addGroup 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : AddGroup (G ⧸ N)
• AddCon.addSubgroup_quotientAddGroupCon 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.Normal] : (QuotientAddGroup.con H).addSubgroup = H
• QuotientAddGroup.con 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : AddCon G
• QuotientAddGroup.instNormalAddSubgroup 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (c : AddCon G) : c.addSubgroup.Normal
• QuotientAddGroup.eq_iff_sub_mem 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] {N : AddSubgroup G} [nN : N.Normal] {x y : G} : ↑x = ↑y ↔ x - y ∈ N
• AddSubgroup.orderIsoAddCon 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] : { N // N.Normal } ≃o AddCon G
• QuotientAddGroup.ker_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : (QuotientAddGroup.mk' N).ker = N
• QuotientAddGroup.con_mono 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] {N M : AddSubgroup G} [hN : N.Normal] [hM : M.Normal] (h : N ≤ M) : QuotientAddGroup.con N ≤ QuotientAddGroup.con M
• QuotientAddGroup.con_le_iff 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] {N M : AddSubgroup G} [N.Normal] [M.Normal] : QuotientAddGroup.con N ≤ QuotientAddGroup.con M ↔ N ≤ M
• QuotientAddGroup.mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : G →+ G ⧸ N
• QuotientAddGroup.preimage_image_coe 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (s : Set G) : QuotientAddGroup.mk ⁻¹' QuotientAddGroup.mk '' s = ↑N + s
• QuotientAddGroup.range_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : (QuotientAddGroup.mk' N).range = ⊤
• QuotientAddGroup.map_mk'_self 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : AddSubgroup.map (QuotientAddGroup.mk' N) N = ⊥
• QuotientAddGroup.mk_neg 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) : ↑(-a) = -↑a
• QuotientAddGroup.mk_zero 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : ↑0 = 0
• QuotientAddGroup.eq_zero_iff 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] {N : AddSubgroup G} [N.Normal] (x : G) : ↑x = 0 ↔ x ∈ N
• QuotientAddGroup.mk_sub 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a b : G) : ↑(a - b) = ↑a - ↑b
• QuotientAddGroup.mk_zsmul 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (n : ℤ) : ↑(n • a) = n • ↑a
• 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.image_coe 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : QuotientAddGroup.mk '' ↑N = 0
• QuotientAddGroup.mk_nsmul 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (n : ℕ) : ↑(n • a) = n • ↑a
• QuotientAddGroup.image_coe_inj 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {s t : Set G} : QuotientAddGroup.mk '' s = QuotientAddGroup.mk '' t ↔ ↑N + s = ↑N + t
• 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.mk_add 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a b : G) : ↑(a + b) = ↑a + ↑b
• 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.injective_lift_iff 📋 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) : Function.Injective ⇑(QuotientAddGroup.lift N φ HN) ↔ N = φ.ker
• 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.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
• AddSubgroup.orderIsoAddCon_apply 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : { N // N.Normal }) : AddSubgroup.orderIsoAddCon N = QuotientAddGroup.con ↑N
• 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
• QuotientAddGroup.addMonoidHom_ext_iff 📋 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} : f = g ↔ f.comp (QuotientAddGroup.mk' N) = g.comp (QuotientAddGroup.mk' N)
• QuotientAddGroup.congr 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') : G ⧸ G' ≃+ H ⧸ H'
• QuotientAddGroup.map_mk 📋 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) (x : G) : (QuotientAddGroup.map N M f h) ↑x = ↑(f x)
• QuotientAddGroup.map_surjective_of_surjective 📋 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) (hf : Function.Surjective (QuotientAddGroup.mk ∘ ⇑f)) (h : N ≤ AddSubgroup.comap f M) : Function.Surjective ⇑(QuotientAddGroup.map N M f h)
• QuotientAddGroup.liftEquiv_coe 📋 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 : G) : (QuotientAddGroup.liftEquiv N hφ HN) ↑g = φ g
• QuotientAddGroup.liftEquiv_mk 📋 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 : G) : (QuotientAddGroup.liftEquiv N hφ HN) ↑g = φ g
• AddSubgroup.orderIsoAddCon_symm_apply_coe 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (c : AddCon G) : ↑((RelIso.symm AddSubgroup.orderIsoAddCon) c) = c.addSubgroup
• QuotientAddGroup.map_mk' 📋 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) (x : G) : (QuotientAddGroup.map N M f h) ((QuotientAddGroup.mk' N) x) = ↑(f x)
• QuotientAddGroup.mk'_comp_subtype 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : (QuotientAddGroup.mk' N).comp N.subtype = 0
• QuotientAddGroup.map_comp_map 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] {I : Type u_5} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [M.Normal] [O.Normal] (f : G →+ H) (g : H →+ I) (hf : N ≤ AddSubgroup.comap f M) (hg : M ≤ AddSubgroup.comap g O) (hgf : N ≤ AddSubgroup.comap (g.comp f) O := ⋯) : (QuotientAddGroup.map M O g hg).comp (QuotientAddGroup.map N M f hf) = QuotientAddGroup.map N O (g.comp f) hgf
• QuotientAddGroup.ker_le_range_iff 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {H : Type u_2} {I : Type u_3} [AddGroup G] [AddGroup H] [AddZeroClass I] (f : G →+ H) [f.range.Normal] (g : H →+ I) : g.ker ≤ f.range ↔ (QuotientAddGroup.mk' f.range).comp g.ker.subtype = 0
• QuotientAddGroup.map_map 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (N : AddSubgroup G) [nN : N.Normal] {I : Type u_5} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [M.Normal] [O.Normal] (f : G →+ H) (g : H →+ I) (hf : N ≤ AddSubgroup.comap f M) (hg : M ≤ AddSubgroup.comap g O) (hgf : N ≤ AddSubgroup.comap (g.comp f) O := ⋯) (x : G ⧸ N) : (QuotientAddGroup.map M O g hg) ((QuotientAddGroup.map N M f hf) x) = (QuotientAddGroup.map N O (g.comp f) hgf) x
• QuotientAddGroup.fg 📋 Mathlib.GroupTheory.Finiteness
  {G : Type u_3} [AddGroup G] [AddGroup.FG G] (N : AddSubgroup G) [N.Normal] : AddGroup.FG (G ⧸ N)
• instNormalAddCommutator 📋 Mathlib.GroupTheory.Commutator.Basic
  (G : Type u_1) [AddGroup G] : (addCommutator G).Normal
• AddSubgroup.Normal.of_addCommutator_le 📋 Mathlib.GroupTheory.Commutator.Basic
  (G : Type u_1) [AddGroup G] {H : AddSubgroup G} (h : addCommutator G ≤ H) : H.Normal
• AddSubgroup.addCommutator_normal 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) [h₁ : H₁.Normal] [h₂ : H₂.Normal] : ⁅H₁, H₂⁆.Normal
• AddSubgroup.addCommutator_le_left 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) [H₁.Normal] : ⁅H₁, H₂⁆ ≤ H₁
• AddSubgroup.addCommutator_le_right 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) [h : H₂.Normal] : ⁅H₁, H₂⁆ ≤ H₂
• AddSubgroup.addCommutator_top_left_le_iff 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : ⁅⊤, H⁆ ≤ H ↔ H.Normal
• AddSubgroup.addCommutator_top_right_le_iff 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : ⁅H, ⊤⁆ ≤ H ↔ H.Normal
• AddSubgroup.addCommutator_le_inf 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) [H₁.Normal] [H₂.Normal] : ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂
• AddSubgroup.Normal.addCommutator_le_of_self_sup_commutative_eq_top 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [AddGroup G] {N : AddSubgroup G} [N.Normal] {H : AddSubgroup G} (hHN : N ⊔ H = ⊤) (hH : IsAddCommutative ↥H) : addCommutator G ≤ N
• AddSubgroup.addCommutator_def' 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) [H₁.Normal] [H₂.Normal] : ⁅H₁, H₂⁆ = AddSubgroup.normalClosure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}
• AddSubgroup.addCommutator_sup_left 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [AddGroup G] (N H K : AddSubgroup G) [N.Normal] : ⁅N, H ⊔ K⁆ = ⁅N, H⁆ ⊔ ⁅N, K⁆
• AddSubgroup.addCommutator_sup_right 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [AddGroup G] (H K N : AddSubgroup G) [N.Normal] : ⁅H ⊔ K, N⁆ = ⁅H, N⁆ ⊔ ⁅K, N⁆
• AddSubgroup.Normal.quotient_commutative_iff_addCommutator_le 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [AddGroup G] {N : AddSubgroup G} [N.Normal] : IsAddCommutative (G ⧸ N) ↔ addCommutator G ≤ N
• AddSubgroup.normal_addSubgroupOf_addCommutator_sup 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) : (⁅H₁, H₂⁆.addSubgroupOf (H₁ ⊔ H₂)).Normal
• fixedPointsSubAddOfNormal 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {H : AddSubgroup G} [hH : H.Normal] : SubAddAction G α
• vadd_mem_fixedPoints_of_normal 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {H : AddSubgroup G} [hH : H.Normal] (g : G) {a : α} (ha : a ∈ AddAction.fixedPoints (↥H) α) : g +ᵥ a ∈ AddAction.fixedPoints (↥H) α
• eq_addCosets_of_normal 📋 Mathlib.GroupTheory.Coset.Basic
  {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (N : s.Normal) (g : α) : g +ᵥ ↑s = AddOpposite.op g +ᵥ ↑s
• normal_of_eq_addCosets 📋 Mathlib.GroupTheory.Coset.Basic
  {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (h : ∀ (g : α), g +ᵥ ↑s = AddOpposite.op g +ᵥ ↑s) : s.Normal
• normal_iff_eq_addCosets 📋 Mathlib.GroupTheory.Coset.Basic
  {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : s.Normal ↔ ∀ (g : α), g +ᵥ ↑s = AddOpposite.op g +ᵥ ↑s
• QuotientAddGroup.map_normal 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] : (AddSubgroup.map (QuotientAddGroup.mk' N) M).Normal
• QuotientAddGroup.le_comap_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [N.Normal] (H : AddSubgroup (G ⧸ N)) : N ≤ AddSubgroup.comap (QuotientAddGroup.mk' N) H
• QuotientAddGroup.comap_map_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N H : AddSubgroup G) [N.Normal] : AddSubgroup.comap (QuotientAddGroup.mk' N) (AddSubgroup.map (QuotientAddGroup.mk' N) H) = N ⊔ H
• QuotientAddGroup.comapMk'OrderIso 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [hn : N.Normal] : AddSubgroup (G ⧸ N) ≃o { H // N ≤ H }
• QuotientAddGroup.quotientAddEquivOfEq 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] {M N : AddSubgroup G} [M.Normal] [N.Normal] (h : M = N) : G ⧸ M ≃+ G ⧸ N
• QuotientAddGroup.mk_int_mul 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {R : Type u_1} [NonAssocRing R] (N : AddSubgroup R) [N.Normal] (n : ℤ) (a : R) : ↑(↑n * a) = n • ↑a
• QuotientAddGroup.mk_nat_mul 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {R : Type u_1} [NonAssocRing R] (N : AddSubgroup R) [N.Normal] (n : ℕ) (a : R) : ↑(↑n * a) = n • ↑a
• QuotientAddGroup.strictMono_comap_prod_map 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : StrictMono fun H => (AddSubgroup.comap N.subtype H, AddSubgroup.map (QuotientAddGroup.mk' N) H)
• QuotientAddGroup.prodAddEquiv 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (A : AddSubgroup G) (B : AddSubgroup H) [A.Normal] [B.Normal] : (G × H) ⧸ A.prod B ≃+ (G ⧸ A) × H ⧸ B
• QuotientAddGroup.comap_comap_center 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] {H₁ : AddSubgroup G} [H₁.Normal] {H₂ : AddSubgroup (G ⧸ H₁)} [H₂.Normal] : AddSubgroup.comap (QuotientAddGroup.mk' H₁) (AddSubgroup.comap (QuotientAddGroup.mk' H₂) (AddSubgroup.center ((G ⧸ H₁) ⧸ H₂))) = AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.comap (QuotientAddGroup.mk' H₁) H₂)) (AddSubgroup.center (G ⧸ AddSubgroup.comap (QuotientAddGroup.mk' H₁) H₂))
• QuotientAddGroup.quotientQuotientEquivQuotientAux 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ AddSubgroup.map (QuotientAddGroup.mk' N) M →+ G ⧸ M
• QuotientAddGroup.quotientAddEquivOfEq_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] {M N : AddSubgroup G} [M.Normal] [N.Normal] (h : M = N) (x : G) : (QuotientAddGroup.quotientAddEquivOfEq h) ↑x = ↑x
• QuotientAddGroup.sound 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (U : Set (G ⧸ N)) (g : ↥N.op) : g +ᵥ ⇑(QuotientAddGroup.mk' N) ⁻¹' U = ⇑(QuotientAddGroup.mk' N) ⁻¹' U
• QuotientAddGroup.quotientQuotientEquivQuotient 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ AddSubgroup.map (QuotientAddGroup.mk' N) M ≃+ G ⧸ M
• QuotientAddGroup.quotientMapAddSubgroupOfOfLe 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] {A' A B' B : AddSubgroup G} [_hAN : (A'.addSubgroupOf A).Normal] [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) : ↥A ⧸ A'.addSubgroupOf A →+ ↥B ⧸ B'.addSubgroupOf B
• QuotientAddGroup.equivQuotientAddSubgroupOfOfEq 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] {A' A B' B : AddSubgroup G} [hAN : (A'.addSubgroupOf A).Normal] [hBN : (B'.addSubgroupOf B).Normal] (h' : A' = B') (h : A = B) : ↥A ⧸ A'.addSubgroupOf A ≃+ ↥B ⧸ B'.addSubgroupOf B
• QuotientAddGroup.quotientQuotientEquivQuotientAux_mk_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) (x : G) : (QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x
• QuotientAddGroup.quotientQuotientEquivQuotientAux_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) (x : G ⧸ N) : (QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) ↑x = (QuotientAddGroup.map N M (AddMonoidHom.id G) h) x
• QuotientAddGroup.prodAddEquiv_apply 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (A : AddSubgroup G) (B : AddSubgroup H) [A.Normal] [B.Normal] (q : (G × H) ⧸ A.prod B) : (QuotientAddGroup.prodAddEquiv A B) q = Quotient.liftOn' q (fun x => (↑x.1, ↑x.2)) ⋯
• AddMonoidHom.domRestrictHomKerEquiv 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (A : Type u_1) [AddCommGroup A] (H : AddSubgroup G) [H.Normal] : ↥(AddMonoidHom.domRestrictHom H A).ker ≃+ (G ⧸ H →+ A)
• AddMonoidHom.restrictHomKerEquiv 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (A : Type u_1) [AddCommGroup A] (H : AddSubgroup G) [H.Normal] : ↥(AddMonoidHom.domRestrictHom H A).ker ≃+ (G ⧸ H →+ A)
• QuotientAddGroup.prodAddEquiv_symm_apply 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (A : AddSubgroup G) (B : AddSubgroup H) [A.Normal] [B.Normal] (q : (G ⧸ A) × H ⧸ B) : (QuotientAddGroup.prodAddEquiv A B).symm q = Quotient.liftOn₂' q.1 q.2 (fun g h => ↑(g, h)) ⋯
• QuotientAddGroup.quotientQuotientEquivQuotient_apply_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) (x : G) : (QuotientAddGroup.quotientQuotientEquivQuotient N M h) ↑↑x = ↑x
• QuotientAddGroup.quotientInfEquivSumNormalQuotient 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (H N : AddSubgroup G) [hN : N.Normal] : ↥H ⧸ N.addSubgroupOf H ≃+ ↥(H ⊔ N) ⧸ N.addSubgroupOf (H ⊔ N)
• QuotientAddGroup.quotientQuotientEquivQuotient_symm_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) (x : G) : (QuotientAddGroup.quotientQuotientEquivQuotient N M h).symm ↑x = ↑↑x
• QuotientAddGroup.quotientMapAddSubgroupOfOfLe_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] {A' A B' B : AddSubgroup G} [_hAN : (A'.addSubgroupOf A).Normal] [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) (x : ↥A) : (QuotientAddGroup.quotientMapAddSubgroupOfOfLe h' h) ↑x = ↑((AddSubgroup.inclusion h) x)
• AddGroup.fintypeOfDomOfCoker 📋 Mathlib.GroupTheory.QuotientGroup.Finite
  {F : Type u_1} {G : Type u_2} [AddGroup F] [AddGroup G] [Fintype F] (f : F →+ G) [f.range.Normal] [Fintype (G ⧸ f.range)] : Fintype G
• AddAction.right_quotientAction' 📋 Mathlib.GroupTheory.GroupAction.Quotient
  {G : Type u} [AddGroup G] (H : AddSubgroup G) [hH : H.Normal] : AddAction.QuotientAction Gᵃᵒᵖ H
• AddAction.coe_quotient_vadd 📋 Mathlib.GroupTheory.GroupAction.Quotient
  {G : Type u} {X : Type v} [AddGroup G] {H : AddSubgroup G} [H.Normal] [VAdd G X] [AddAction (G ⧸ H) X] [VAddAssocClass G (G ⧸ H) X] (g : G) (x : X) : ↑g +ᵥ x = g +ᵥ x
• AddSubgroup.relIndex_dvd_index_of_normal 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [H.Normal] : H.relIndex K ∣ H.index
• AddSubgroup.relIndex_sup_left 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [K.Normal] : K.relIndex (K ⊔ H) = K.relIndex H
• AddSubgroup.relIndex_sup_right 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [K.Normal] : K.relIndex (H ⊔ K) = K.relIndex H
• AddSubgroup.nsmul_index_mem 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_6} [AddGroup G] (H : AddSubgroup G) [H.Normal] (g : G) : H.index • g ∈ H
• AddSubgroup.nsmul_relIndex_mem 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_6} [AddGroup G] (H : AddSubgroup G) [H.Normal] {K : AddSubgroup G} {g : G} (hg : g ∈ K) : H.relIndex K • g ∈ H
• AddSubgroup.is_normal_topologicalClosure 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_3} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] : N.topologicalClosure.Normal
• QuotientAddGroup.instIsTopologicalAddGroup 📋 Mathlib.Topology.Algebra.Group.Quotient
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] : IsTopologicalAddGroup (G ⧸ N)
• QuotientAddGroup.instT3Space 📋 Mathlib.Topology.Algebra.Group.Quotient
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] [hN : IsClosed ↑N] : T3Space (G ⧸ N)
• QuotientAddGroup.completeSpace_left' 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [FirstCountableTopology G] (N : AddSubgroup G) [N.Normal] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)
• QuotientAddGroup.completeSpace_right' 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [FirstCountableTopology G] (N : AddSubgroup G) [N.Normal] [CompleteSpace G] : CompleteSpace (G ⧸ N)
• QuotientAddGroup.completeSpace_left 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u_1) [AddGroup G] [us : UniformSpace G] [IsLeftUniformAddGroup G] [FirstCountableTopology G] (N : AddSubgroup G) [N.Normal] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)
• QuotientAddGroup.completeSpace_right 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  (G : Type u_1) [AddGroup G] [us : UniformSpace G] [IsRightUniformAddGroup G] [FirstCountableTopology G] (N : AddSubgroup G) [N.Normal] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)
• AddGroup.exponent_quotient_dvd 📋 Mathlib.GroupTheory.Exponent
  {G : Type u} [AddGroup G] (H : AddSubgroup G) [H.Normal] : AddMonoid.exponent (G ⧸ H) ∣ AddMonoid.exponent G
• IsSimpleAddGroup.eq_bot_or_eq_top_of_normal 📋 Mathlib.GroupTheory.Subgroup.Simple
  {A : Type u_2} {inst✝ : AddGroup A} [self : IsSimpleAddGroup A] (H : AddSubgroup A) : H.Normal → H = ⊥ ∨ H = ⊤
• AddSubgroup.Normal.eq_bot_or_eq_top 📋 Mathlib.GroupTheory.Subgroup.Simple
  {G : Type u_1} [AddGroup G] [IsSimpleAddGroup G] {H : AddSubgroup G} (Hn : H.Normal) : H = ⊥ ∨ H = ⊤
• IsSimpleAddGroup.mk 📋 Mathlib.GroupTheory.Subgroup.Simple
  {A : Type u_2} [AddGroup A] [toNontrivial : Nontrivial A] (eq_bot_or_eq_top_of_normal : ∀ (H : AddSubgroup A), H.Normal → H = ⊥ ∨ H = ⊤) : IsSimpleAddGroup A
• isSimpleAddGroup_iff 📋 Mathlib.GroupTheory.Subgroup.Simple
  (A : Type u_2) [AddGroup A] : IsSimpleAddGroup A ↔ Nontrivial A ∧ ∀ (H : AddSubgroup A), H.Normal → H = ⊥ ∨ H = ⊤
• AddSubgroup.isSimpleAddGroup_iff 📋 Mathlib.GroupTheory.Subgroup.Simple
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : IsSimpleAddGroup ↥H ↔ H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.addSubgroupOf H).Normal → H' = ⊥ ∨ H' = H
• QuotientAddGroup.borelSpace 📋 Mathlib.MeasureTheory.Constructions.Polish.Basic
  {G : Type u_3} [TopologicalSpace G] [PolishSpace G] [AddGroup G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {N : AddSubgroup G} [N.Normal] [IsClosed ↑N] : BorelSpace (G ⧸ N)
• AddSubgroup.Normal.pathComponentZero 📋 Mathlib.Topology.Connected.PathConnected
  (G : Type u_4) [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] : (AddSubgroup.pathComponentZero G).Normal
• OpenNormalAddSubgroup.instNormal 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u} [AddGroup G] [TopologicalSpace G] (H : OpenNormalAddSubgroup G) : (↑H.toOpenAddSubgroup).Normal
• OpenNormalAddSubgroup.isNormal' 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u} [AddGroup G] [TopologicalSpace G] (self : OpenNormalAddSubgroup G) : (↑self.toOpenAddSubgroup).Normal
• OpenNormalAddSubgroup.mk 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u} [AddGroup G] [TopologicalSpace G] (toOpenAddSubgroup : OpenAddSubgroup G) (isNormal' : (↑toOpenAddSubgroup).Normal := by infer_instance) : OpenNormalAddSubgroup G
• MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addHaarMeasure_quotient 📋 Mathlib.MeasureTheory.Measure.Haar.Quotient
  {G : Type u_1} [AddGroup G] [MeasurableSpace G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [PolishSpace G] {Γ : AddSubgroup G} [Γ.Normal] [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} [Countable ↥Γ] (ν : MeasureTheory.Measure G) [ν.IsAddHaarMeasure] [ν.IsAddRightInvariant] [LocallyCompactSpace G] [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] [i : MeasureTheory.HasAddFundamentalDomain (↥Γ.op) G ν] [MeasureTheory.IsFiniteMeasure μ] : μ.IsAddHaarMeasure
• MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addInvariantMeasure_quotient 📋 Mathlib.MeasureTheory.Measure.Haar.Quotient
  {G : Type u_1} [AddGroup G] [MeasurableSpace G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [PolishSpace G] {Γ : AddSubgroup G} [Γ.Normal] [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} (ν : MeasureTheory.Measure G) [ν.IsAddLeftInvariant] [hasFun : MeasureTheory.HasAddFundamentalDomain (↥Γ.op) G ν] [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] : μ.IsAddLeftInvariant
• IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure 📋 Mathlib.MeasureTheory.Measure.Haar.Quotient
  {G : Type u_1} [AddGroup G] [MeasurableSpace G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [PolishSpace G] {Γ : AddSubgroup G} [Γ.Normal] [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)] [Countable ↥Γ] (ν : MeasureTheory.Measure G) [ν.IsAddHaarMeasure] [ν.IsAddRightInvariant] [MeasureTheory.SigmaFinite ν] (K : TopologicalSpace.PositiveCompacts (G ⧸ Γ)) {𝓕 : Set G} (h𝓕 : MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 ν) (h𝓕_finite : ν 𝓕 ≠ ⊤) : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν (ν (QuotientAddGroup.mk ⁻¹' ↑K ∩ 𝓕) • MeasureTheory.Measure.addHaarMeasure K)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c