Subgroups

This file defines multiplicative and additive subgroups as an extension of submonoids, in a bundled form (unbundled subgroups are in Deprecated/Subgroups.lean).

Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.

Main definitions

Notation used here:

• G N are Groups

• A is an AddGroup

• H K are Subgroups of G or AddSubgroups of A

• x is an element of type G or type A

• f g : N →* G are group homomorphisms

• s k are sets of elements of type G

Definitions in the file:

• Subgroup G : the type of subgroups of a group G

• AddSubgroup A : the type of subgroups of an additive group A

• Subgroup.subtype : the natural group homomorphism from a subgroup of group G to G

Implementation notes

Subgroup inclusion is denoted ≤ rather than ⊆, although ∈ is defined as membership of a subgroup's underlying set.

Tags

subgroup, subgroups

class InvMemClass (S : Type u_3) (G : outParam (Type u_4)) [Inv G] [SetLike S G] : Prop

InvMemClass S G states S is a type of subsets s ⊆ G closed under inverses.

• inv_mem {s : S} {x : G} : x ∈ s → x⁻¹ ∈ s

  s is closed under inverses

class NegMemClass (S : Type u_3) (G : outParam (Type u_4)) [Neg G] [SetLike S G] : Prop

NegMemClass S G states S is a type of subsets s ⊆ G closed under negation.

• neg_mem {s : S} {x : G} : x ∈ s → -x ∈ s

  s is closed under negation

class SubgroupClass (S : Type u_3) (G : outParam (Type u_4)) [DivInvMonoid G] [SetLike S G] extends SubmonoidClass S G, InvMemClass S G : Prop

SubgroupClass S G states S is a type of subsets s ⊆ G that are subgroups of G.

• mul_mem {s : S} {a b : G} : a ∈ s → b ∈ s → a * b ∈ s
• one_mem (s : S) : 1 ∈ s
• inv_mem {s : S} {x : G} : x ∈ s → x⁻¹ ∈ s

class AddSubgroupClass (S : Type u_3) (G : outParam (Type u_4)) [SubNegMonoid G] [SetLike S G] extends AddSubmonoidClass S G, NegMemClass S G : Prop

AddSubgroupClass S G states S is a type of subsets s ⊆ G that are additive subgroups of G.

• add_mem {s : S} {a b : G} : a ∈ s → b ∈ s → a + b ∈ s
• zero_mem (s : S) : 0 ∈ s
• neg_mem {s : S} {x : G} : x ∈ s → -x ∈ s

@[simp]

theorem inv_mem_iff {S : Type u_3} {G : Type u_4} [InvolutiveInv G] {x✝ : SetLike S G} [InvMemClass S G] {H : S} {x : G} : x⁻¹ ∈ H ↔ x ∈ H

@[simp]

theorem neg_mem_iff {S : Type u_3} {G : Type u_4} [InvolutiveNeg G] {x✝ : SetLike S G} [NegMemClass S G] {H : S} {x : G} : -x ∈ H ↔ x ∈ H

theorem div_mem {M : Type u_3} {S : Type u_4} [DivInvMonoid M] [SetLike S M] [hSM : SubgroupClass S M] {H : S} {x y : M} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H

A subgroup is closed under division.

theorem sub_mem {M : Type u_3} {S : Type u_4} [SubNegMonoid M] [SetLike S M] [hSM : AddSubgroupClass S M] {H : S} {x y : M} (hx : x ∈ H) (hy : y ∈ H) : x - y ∈ H

An additive subgroup is closed under subtraction.

theorem zpow_mem {M : Type u_3} {S : Type u_4} [DivInvMonoid M] [SetLike S M] [hSM : SubgroupClass S M] {K : S} {x : M} (hx : x ∈ K) (n : ℤ) : x ^ n ∈ K

theorem zsmul_mem {M : Type u_3} {S : Type u_4} [SubNegMonoid M] [SetLike S M] [hSM : AddSubgroupClass S M] {K : S} {x : M} (hx : x ∈ K) (n : ℤ) : n • x ∈ K

theorem exists_inv_mem_iff_exists_mem {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] {P : G → Prop} : (∃ x ∈ H, P x⁻¹) ↔ ∃ x ∈ H, P x

theorem exists_neg_mem_iff_exists_mem {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] {P : G → Prop} : (∃ x ∈ H, P (-x)) ↔ ∃ x ∈ H, P x

theorem mul_mem_cancel_right {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H

theorem add_mem_cancel_right {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] {x y : G} (h : x ∈ H) : y + x ∈ H ↔ y ∈ H

theorem mul_mem_cancel_left {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H

theorem add_mem_cancel_left {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] {x y : G} (h : x ∈ H) : x + y ∈ H ↔ y ∈ H

instance InvMemClass.inv {G : Type u_1} {S : Type u_2} [Inv G] [SetLike S G] [InvMemClass S G] {H : S} : Inv ↥H

A subgroup of a group inherits an inverse.

Equations

• InvMemClass.inv = { inv := fun (a : ↥H) => ⟨(↑a)⁻¹, ⋯⟩ }

instance NegMemClass.neg {G : Type u_1} {S : Type u_2} [Neg G] [SetLike S G] [NegMemClass S G] {H : S} : Neg ↥H

An additive subgroup of an AddGroup inherits an inverse.

Equations

• NegMemClass.neg = { neg := fun (a : ↥H) => ⟨-↑a, ⋯⟩ }

@[simp]

theorem InvMemClass.coe_inv {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] (x : ↥H) : ↑x⁻¹ = (↑x)⁻¹

@[simp]

theorem NegMemClass.coe_neg {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : ↥H) : ↑(-x) = -↑x

theorem SubgroupClass.subset_union {G : Type u_1} [Group G] {S : Type u_4} [SetLike S G] [SubgroupClass S G] {H K L : S} : ↑H ⊆ ↑K ∪ ↑L ↔ H ≤ K ∨ H ≤ L

theorem AddSubgroupClass.subset_union {G : Type u_1} [AddGroup G] {S : Type u_4} [SetLike S G] [AddSubgroupClass S G] {H K L : S} : ↑H ⊆ ↑K ∪ ↑L ↔ H ≤ K ∨ H ≤ L

instance SubgroupClass.div {G : Type u_1} {S : Type u_2} [DivInvMonoid G] [SetLike S G] [SubgroupClass S G] {H : S} : Div ↥H

A subgroup of a group inherits a division

Equations

• SubgroupClass.div = { div := fun (a b : ↥H) => ⟨↑a / ↑b, ⋯⟩ }

instance AddSubgroupClass.sub {G : Type u_1} {S : Type u_2} [SubNegMonoid G] [SetLike S G] [AddSubgroupClass S G] {H : S} : Sub ↥H

An additive subgroup of an AddGroup inherits a subtraction.

Equations

• AddSubgroupClass.sub = { sub := fun (a b : ↥H) => ⟨↑a - ↑b, ⋯⟩ }

instance AddSubgroupClass.zsmul {M : Type u_5} {S : Type u_6} [SubNegMonoid M] [SetLike S M] [AddSubgroupClass S M] {H : S} : SMul ℤ ↥H

An additive subgroup of an AddGroup inherits an integer scaling.

Equations

• AddSubgroupClass.zsmul = { smul := fun (n : ℤ) (a : ↥H) => ⟨n • ↑a, ⋯⟩ }

instance SubgroupClass.zpow {M : Type u_5} {S : Type u_6} [DivInvMonoid M] [SetLike S M] [SubgroupClass S M] {H : S} : Pow ↥H ℤ

A subgroup of a group inherits an integer power.

Equations

• SubgroupClass.zpow = { pow := fun (a : ↥H) (n : ℤ) => ⟨↑a ^ n, ⋯⟩ }

@[simp]

theorem SubgroupClass.coe_div {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] (x y : ↥H) : ↑(x / y) = ↑x / ↑y

@[simp]

theorem AddSubgroupClass.coe_sub {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] (x y : ↥H) : ↑(x - y) = ↑x - ↑y

@[instance 75]

instance SubgroupClass.toGroup {G : Type u_1} [Group G] {S : Type u_4} (H : S) [SetLike S G] [SubgroupClass S G] : Group ↥H

A subgroup of a group inherits a group structure.

Equations

• One or more equations did not get rendered due to their size.

@[instance 75]

instance AddSubgroupClass.toAddGroup {G : Type u_1} [AddGroup G] {S : Type u_4} (H : S) [SetLike S G] [AddSubgroupClass S G] : AddGroup ↥H

An additive subgroup of an AddGroup inherits an AddGroup structure.

Equations

• One or more equations did not get rendered due to their size.

@[instance 75]

instance SubgroupClass.toCommGroup {S : Type u_4} (H : S) {G : Type u_5} [CommGroup G] [SetLike S G] [SubgroupClass S G] : CommGroup ↥H

A subgroup of a CommGroup is a CommGroup.

Equations

• SubgroupClass.toCommGroup H = { toGroup := SubgroupClass.toGroup H, mul_comm := ⋯ }

@[instance 75]

instance AddSubgroupClass.toAddCommGroup {S : Type u_4} (H : S) {G : Type u_5} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : AddCommGroup ↥H

An additive subgroup of an AddCommGroup is an AddCommGroup.

Equations

• AddSubgroupClass.toAddCommGroup H = { toAddGroup := AddSubgroupClass.toAddGroup H, add_comm := ⋯ }

def SubgroupClass.subtype {G : Type u_1} [Group G] {S : Type u_4} (H : S) [SetLike S G] [SubgroupClass S G] : ↥H →* G

The natural group hom from a subgroup of group G to G.

Equations

• ↑H = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }

def AddSubgroupClass.subtype {G : Type u_1} [AddGroup G] {S : Type u_4} (H : S) [SetLike S G] [AddSubgroupClass S G] : ↥H →+ G

The natural group hom from an additive subgroup of AddGroup G to G.

Equations

• ↑H = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem SubgroupClass.subtype_apply {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] (x : ↥H) : ↑H x = ↑x

@[simp]

theorem AddSubgroupClass.subtype_apply {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : ↥H) : ↑H x = ↑x

theorem SubgroupClass.subtype_injective {G : Type u_1} [Group G] {S : Type u_4} (H : S) [SetLike S G] [SubgroupClass S G] : Function.Injective ⇑↑H

theorem AddSubgroupClass.subtype_injective {G : Type u_1} [AddGroup G] {S : Type u_4} (H : S) [SetLike S G] [AddSubgroupClass S G] : Function.Injective ⇑↑H

@[simp]

theorem SubgroupClass.coe_subtype {G : Type u_1} [Group G] {S : Type u_4} (H : S) [SetLike S G] [SubgroupClass S G] : ⇑↑H = Subtype.val

@[simp]

theorem AddSubgroupClass.coe_subtype {G : Type u_1} [AddGroup G] {S : Type u_4} (H : S) [SetLike S G] [AddSubgroupClass S G] : ⇑↑H = Subtype.val

@[deprecated SubgroupClass.coe_subtype (since := "2025-02-18")]

theorem SubgroupClass.coeSubtype {G : Type u_1} [Group G] {S : Type u_4} (H : S) [SetLike S G] [SubgroupClass S G] : ⇑↑H = Subtype.val

Alias of SubgroupClass.coe_subtype.

@[deprecated AddSubgroupClass.coe_subtype (since := "2025-02-18")]

theorem AddSubgroupClass.coeSubtype {G : Type u_1} [AddGroup G] {S : Type u_4} (H : S) [SetLike S G] [AddSubgroupClass S G] : ⇑↑H = Subtype.val

Alias of AddSubgroupClass.coe_subtype.

@[simp]

theorem SubgroupClass.coe_pow {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] (x : ↥H) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

@[simp]

theorem AddSubgroupClass.coe_nsmul {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : ↥H) (n : ℕ) : ↑(n • x) = n • ↑x

@[simp]

theorem SubgroupClass.coe_zpow {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] (x : ↥H) (n : ℤ) : ↑(x ^ n) = ↑x ^ n

@[simp]

theorem AddSubgroupClass.coe_zsmul {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : ↥H) (n : ℤ) : ↑(n • x) = n • ↑x

def SubgroupClass.inclusion {G : Type u_1} [Group G] {S : Type u_4} [SetLike S G] [SubgroupClass S G] {H K : S} (h : H ≤ K) : ↥H →* ↥K

The inclusion homomorphism from a subgroup H contained in K to K.

Equations

• SubgroupClass.inclusion h = MonoidHom.mk' (fun (x : ↥H) => ⟨↑x, ⋯⟩) ⋯

def AddSubgroupClass.inclusion {G : Type u_1} [AddGroup G] {S : Type u_4} [SetLike S G] [AddSubgroupClass S G] {H K : S} (h : H ≤ K) : ↥H →+ ↥K

The inclusion homomorphism from an additive subgroup H contained in K to K.

Equations

• AddSubgroupClass.inclusion h = AddMonoidHom.mk' (fun (x : ↥H) => ⟨↑x, ⋯⟩) ⋯

@[simp]

theorem SubgroupClass.inclusion_self {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] (x : ↥H) : (inclusion ⋯) x = x

@[simp]

theorem AddSubgroupClass.inclusion_self {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : ↥H) : (inclusion ⋯) x = x

@[simp]

theorem SubgroupClass.inclusion_mk {G : Type u_1} [Group G] {S : Type u_4} {H K : S} [SetLike S G] [SubgroupClass S G] {h : H ≤ K} (x : G) (hx : x ∈ H) : (inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩

@[simp]

theorem AddSubgroupClass.inclusion_mk {G : Type u_1} [AddGroup G] {S : Type u_4} {H K : S} [SetLike S G] [AddSubgroupClass S G] {h : H ≤ K} (x : G) (hx : x ∈ H) : (inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩

theorem SubgroupClass.inclusion_right {G : Type u_1} [Group G] {S : Type u_4} {H K : S} [SetLike S G] [SubgroupClass S G] (h : H ≤ K) (x : ↥K) (hx : ↑x ∈ H) : (inclusion h) ⟨↑x, hx⟩ = x

theorem AddSubgroupClass.inclusion_right {G : Type u_1} [AddGroup G] {S : Type u_4} {H K : S} [SetLike S G] [AddSubgroupClass S G] (h : H ≤ K) (x : ↥K) (hx : ↑x ∈ H) : (inclusion h) ⟨↑x, hx⟩ = x

@[simp]

theorem SubgroupClass.inclusion_inclusion {G : Type u_1} [Group G] {S : Type u_4} {H K : S} [SetLike S G] [SubgroupClass S G] {L : S} (hHK : H ≤ K) (hKL : K ≤ L) (x : ↥H) : (inclusion hKL) ((inclusion hHK) x) = (inclusion ⋯) x

@[simp]

theorem SubgroupClass.coe_inclusion {G : Type u_1} [Group G] {S : Type u_4} [SetLike S G] [SubgroupClass S G] {H K : S} {h : H ≤ K} (a : ↥H) : ↑((inclusion h) a) = ↑a

@[simp]

theorem AddSubgroupClass.coe_inclusion {G : Type u_1} [AddGroup G] {S : Type u_4} [SetLike S G] [AddSubgroupClass S G] {H K : S} {h : H ≤ K} (a : ↥H) : ↑((inclusion h) a) = ↑a

@[simp]

theorem SubgroupClass.subtype_comp_inclusion {G : Type u_1} [Group G] {S : Type u_4} [SetLike S G] [SubgroupClass S G] {H K : S} (hH : H ≤ K) : (↑K).comp (inclusion hH) = ↑H

@[simp]

theorem AddSubgroupClass.subtype_comp_inclusion {G : Type u_1} [AddGroup G] {S : Type u_4} [SetLike S G] [AddSubgroupClass S G] {H K : S} (hH : H ≤ K) : (↑K).comp (inclusion hH) = ↑H

structure Subgroup (G : Type u_3) [Group G] extends Submonoid G : Type u_3

A subgroup of a group G is a subset containing 1, closed under multiplication and closed under multiplicative inverse.

• carrier : Set G
• mul_mem' {a b : G} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• inv_mem' {x : G} : x ∈ self.carrier → x⁻¹ ∈ self.carrier

  G is closed under inverses

structure AddSubgroup (G : Type u_3) [AddGroup G] extends AddSubmonoid G : Type u_3

An additive subgroup of an additive group G is a subset containing 0, closed under addition and additive inverse.

• carrier : Set G
• add_mem' {a b : G} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• neg_mem' {x : G} : x ∈ self.carrier → -x ∈ self.carrier

  G is closed under negation

instance Subgroup.instSetLike {G : Type u_1} [Group G] : SetLike (Subgroup G) G

Equations

• Subgroup.instSetLike = { coe := fun (s : Subgroup G) => s.carrier, coe_injective' := ⋯ }

instance AddSubgroup.instSetLike {G : Type u_1} [AddGroup G] : SetLike (AddSubgroup G) G

Equations

• AddSubgroup.instSetLike = { coe := fun (s : AddSubgroup G) => s.carrier, coe_injective' := ⋯ }

def Subgroup.ofClass {S : Type u_3} {G : Type u_4} [Group G] [SetLike S G] [SubgroupClass S G] (s : S) : Subgroup G

The actual Subgroup obtained from an element of a SubgroupClass

Equations

• Subgroup.ofClass s = { carrier := ↑s, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

def AddSubgroup.ofClass {S : Type u_3} {G : Type u_4} [AddGroup G] [SetLike S G] [AddSubgroupClass S G] (s : S) : AddSubgroup G

The actual AddSubgroup obtained from an element of a AddSubgroupClass

Equations

• AddSubgroup.ofClass s = { carrier := ↑s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem AddSubgroup.coe_ofClass {S : Type u_3} {G : Type u_4} [AddGroup G] [SetLike S G] [AddSubgroupClass S G] (s : S) : ↑(ofClass s) = ↑s

@[simp]

theorem Subgroup.coe_ofClass {S : Type u_3} {G : Type u_4} [Group G] [SetLike S G] [SubgroupClass S G] (s : S) : ↑(ofClass s) = ↑s

@[instance 100]

instance Subgroup.instCanLiftSetCoeAndMemOfNatForallForallForallForallHMulForallForallInv {G : Type u_1} [Group G] : CanLift (Set G) (Subgroup G) SetLike.coe fun (s : Set G) => 1 ∈ s ∧ (∀ {x y : G}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x : G}, x ∈ s → x⁻¹ ∈ s

@[instance 100]

instance AddSubgroup.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallNeg {G : Type u_1} [AddGroup G] : CanLift (Set G) (AddSubgroup G) SetLike.coe fun (s : Set G) => 0 ∈ s ∧ (∀ {x y : G}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ {x : G}, x ∈ s → -x ∈ s

instance Subgroup.instSubgroupClass {G : Type u_1} [Group G] : SubgroupClass (Subgroup G) G

instance AddSubgroup.instAddSubgroupClass {G : Type u_1} [AddGroup G] : AddSubgroupClass (AddSubgroup G) G

theorem Subgroup.mem_carrier {G : Type u_1} [Group G] {s : Subgroup G} {x : G} : x ∈ s.carrier ↔ x ∈ s

theorem AddSubgroup.mem_carrier {G : Type u_1} [AddGroup G] {s : AddSubgroup G} {x : G} : x ∈ s.carrier ↔ x ∈ s

@[simp]

theorem Subgroup.mem_mk {G : Type u_1} [Group G] {s : Set G} {x : G} (h_one : ∀ {a b : G}, a ∈ s → b ∈ s → a * b ∈ s) (h_mul : s 1) (h_inv : ∀ {x : G}, x ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier → x⁻¹ ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier) : x ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul, inv_mem' := h_inv } ↔ x ∈ s

@[simp]

theorem AddSubgroup.mem_mk {G : Type u_1} [AddGroup G] {s : Set G} {x : G} (h_one : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s) (h_mul : s 0) (h_inv : ∀ {x : G}, x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier → -x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier) : x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul, neg_mem' := h_inv } ↔ x ∈ s

@[simp]

theorem Subgroup.coe_set_mk {G : Type u_1} [Group G] {s : Set G} (h_one : ∀ {a b : G}, a ∈ s → b ∈ s → a * b ∈ s) (h_mul : s 1) (h_inv : ∀ {x : G}, x ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier → x⁻¹ ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier) : ↑{ carrier := s, mul_mem' := h_one, one_mem' := h_mul, inv_mem' := h_inv } = s

@[simp]

theorem AddSubgroup.coe_set_mk {G : Type u_1} [AddGroup G] {s : Set G} (h_one : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s) (h_mul : s 0) (h_inv : ∀ {x : G}, x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier → -x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier) : ↑{ carrier := s, add_mem' := h_one, zero_mem' := h_mul, neg_mem' := h_inv } = s

@[simp]

theorem Subgroup.mk_le_mk {G : Type u_1} [Group G] {s t : Set G} (h_one : ∀ {a b : G}, a ∈ s → b ∈ s → a * b ∈ s) (h_mul : s 1) (h_inv : ∀ {x : G}, x ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier → x⁻¹ ∈ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier) (h_one' : ∀ {a b : G}, a ∈ t → b ∈ t → a * b ∈ t) (h_mul' : t 1) (h_inv' : ∀ {x : G}, x ∈ { carrier := t, mul_mem' := h_one', one_mem' := h_mul' }.carrier → x⁻¹ ∈ { carrier := t, mul_mem' := h_one', one_mem' := h_mul' }.carrier) : { carrier := s, mul_mem' := h_one, one_mem' := h_mul, inv_mem' := h_inv } ≤ { carrier := t, mul_mem' := h_one', one_mem' := h_mul', inv_mem' := h_inv' } ↔ s ⊆ t

@[simp]

theorem AddSubgroup.mk_le_mk {G : Type u_1} [AddGroup G] {s t : Set G} (h_one : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s) (h_mul : s 0) (h_inv : ∀ {x : G}, x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier → -x ∈ { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier) (h_one' : ∀ {a b : G}, a ∈ t → b ∈ t → a + b ∈ t) (h_mul' : t 0) (h_inv' : ∀ {x : G}, x ∈ { carrier := t, add_mem' := h_one', zero_mem' := h_mul' }.carrier → -x ∈ { carrier := t, add_mem' := h_one', zero_mem' := h_mul' }.carrier) : { carrier := s, add_mem' := h_one, zero_mem' := h_mul, neg_mem' := h_inv } ≤ { carrier := t, add_mem' := h_one', zero_mem' := h_mul', neg_mem' := h_inv' } ↔ s ⊆ t

@[simp]

theorem Subgroup.coe_toSubmonoid {G : Type u_1} [Group G] (K : Subgroup G) : ↑K.toSubmonoid = ↑K

@[simp]

theorem AddSubgroup.coe_toAddSubmonoid {G : Type u_1} [AddGroup G] (K : AddSubgroup G) : ↑K.toAddSubmonoid = ↑K

@[simp]

theorem Subgroup.mem_toSubmonoid {G : Type u_1} [Group G] (K : Subgroup G) (x : G) : x ∈ K.toSubmonoid ↔ x ∈ K

@[simp]

theorem AddSubgroup.mem_toAddSubmonoid {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (x : G) : x ∈ K.toAddSubmonoid ↔ x ∈ K

theorem Subgroup.toSubmonoid_injective {G : Type u_1} [Group G] : Function.Injective toSubmonoid

theorem AddSubgroup.toAddSubmonoid_injective {G : Type u_1} [AddGroup G] : Function.Injective toAddSubmonoid

@[simp]

theorem Subgroup.toSubmonoid_inj {G : Type u_1} [Group G] {p q : Subgroup G} : p.toSubmonoid = q.toSubmonoid ↔ p = q

@[simp]

theorem AddSubgroup.toAddSubmonoid_inj {G : Type u_1} [AddGroup G] {p q : AddSubgroup G} : p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q

@[deprecated Subgroup.toSubmonoid_inj (since := "2024-12-29")]

theorem Subgroup.toSubmonoid_eq {G : Type u_1} [Group G] {p q : Subgroup G} : p.toSubmonoid = q.toSubmonoid ↔ p = q

Alias of Subgroup.toSubmonoid_inj.

theorem AddSubgroup.toAddSubmonoid_eq {G : Type u_1} [AddGroup G] {p q : AddSubgroup G} : p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q

theorem Subgroup.toSubmonoid_strictMono {G : Type u_1} [Group G] : StrictMono toSubmonoid

theorem AddSubgroup.toAddSubmonoid_strictMono {G : Type u_1} [AddGroup G] : StrictMono toAddSubmonoid

theorem Subgroup.toSubmonoid_mono {G : Type u_1} [Group G] : Monotone toSubmonoid

theorem AddSubgroup.toAddSubmonoid_mono {G : Type u_1} [AddGroup G] : Monotone toAddSubmonoid

@[simp]

theorem Subgroup.toSubmonoid_le {G : Type u_1} [Group G] {p q : Subgroup G} : p.toSubmonoid ≤ q.toSubmonoid ↔ p ≤ q

@[simp]

theorem AddSubgroup.toAddSubmonoid_le {G : Type u_1} [AddGroup G] {p q : AddSubgroup G} : p.toAddSubmonoid ≤ q.toAddSubmonoid ↔ p ≤ q

@[simp]

theorem Subgroup.coe_nonempty {G : Type u_1} [Group G] (s : Subgroup G) : (↑s).Nonempty

@[simp]

theorem AddSubgroup.coe_nonempty {G : Type u_1} [AddGroup G] (s : AddSubgroup G) : (↑s).Nonempty

def Subgroup.copy {G : Type u_1} [Group G] (K : Subgroup G) (s : Set G) (hs : s = ↑K) : Subgroup G

Copy of a subgroup with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations

• K.copy s hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

def AddSubgroup.copy {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = ↑K) : AddSubgroup G

Copy of an additive subgroup with a new carrier equal to the old one. Useful to fix definitional equalities

Equations

• K.copy s hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem Subgroup.coe_copy {G : Type u_1} [Group G] (K : Subgroup G) (s : Set G) (hs : s = ↑K) : ↑(K.copy s hs) = s

@[simp]

theorem AddSubgroup.coe_copy {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = ↑K) : ↑(K.copy s hs) = s

theorem Subgroup.copy_eq {G : Type u_1} [Group G] (K : Subgroup G) (s : Set G) (hs : s = ↑K) : K.copy s hs = K

theorem AddSubgroup.copy_eq {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = ↑K) : K.copy s hs = K

theorem Subgroup.ext {G : Type u_1} [Group G] {H K : Subgroup G} (h : ∀ (x : G), x ∈ H ↔ x ∈ K) : H = K

Two subgroups are equal if they have the same elements.

theorem AddSubgroup.ext {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : ∀ (x : G), x ∈ H ↔ x ∈ K) : H = K

Two AddSubgroups are equal if they have the same elements.

theorem AddSubgroup.ext_iff {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : H = K ↔ ∀ (x : G), x ∈ H ↔ x ∈ K

theorem Subgroup.ext_iff {G : Type u_1} [Group G] {H K : Subgroup G} : H = K ↔ ∀ (x : G), x ∈ H ↔ x ∈ K

theorem Subgroup.one_mem {G : Type u_1} [Group G] (H : Subgroup G) : 1 ∈ H

A subgroup contains the group's 1.

theorem AddSubgroup.zero_mem {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : 0 ∈ H

An AddSubgroup contains the group's 0.

theorem Subgroup.mul_mem {G : Type u_1} [Group G] (H : Subgroup G) {x y : G} : x ∈ H → y ∈ H → x * y ∈ H

A subgroup is closed under multiplication.

theorem AddSubgroup.add_mem {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x y : G} : x ∈ H → y ∈ H → x + y ∈ H

An AddSubgroup is closed under addition.

theorem Subgroup.inv_mem {G : Type u_1} [Group G] (H : Subgroup G) {x : G} : x ∈ H → x⁻¹ ∈ H

A subgroup is closed under inverse.

theorem AddSubgroup.neg_mem {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x : G} : x ∈ H → -x ∈ H

An AddSubgroup is closed under inverse.

theorem Subgroup.div_mem {G : Type u_1} [Group G] (H : Subgroup G) {x y : G} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H

A subgroup is closed under division.

theorem AddSubgroup.sub_mem {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x y : G} (hx : x ∈ H) (hy : y ∈ H) : x - y ∈ H

An AddSubgroup is closed under subtraction.

theorem Subgroup.inv_mem_iff {G : Type u_1} [Group G] (H : Subgroup G) {x : G} : x⁻¹ ∈ H ↔ x ∈ H

theorem AddSubgroup.neg_mem_iff {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x : G} : -x ∈ H ↔ x ∈ H

theorem Subgroup.exists_inv_mem_iff_exists_mem {G : Type u_1} [Group G] (K : Subgroup G) {P : G → Prop} : (∃ x ∈ K, P x⁻¹) ↔ ∃ x ∈ K, P x

theorem AddSubgroup.exists_neg_mem_iff_exists_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {P : G → Prop} : (∃ x ∈ K, P (-x)) ↔ ∃ x ∈ K, P x

theorem Subgroup.mul_mem_cancel_right {G : Type u_1} [Group G] (H : Subgroup G) {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H

theorem AddSubgroup.add_mem_cancel_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x y : G} (h : x ∈ H) : y + x ∈ H ↔ y ∈ H

theorem Subgroup.mul_mem_cancel_left {G : Type u_1} [Group G] (H : Subgroup G) {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H

theorem AddSubgroup.add_mem_cancel_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x y : G} (h : x ∈ H) : x + y ∈ H ↔ y ∈ H

theorem Subgroup.pow_mem {G : Type u_1} [Group G] (K : Subgroup G) {x : G} (hx : x ∈ K) (n : ℕ) : x ^ n ∈ K

theorem AddSubgroup.nsmul_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {x : G} (hx : x ∈ K) (n : ℕ) : n • x ∈ K

theorem Subgroup.zpow_mem {G : Type u_1} [Group G] (K : Subgroup G) {x : G} (hx : x ∈ K) (n : ℤ) : x ^ n ∈ K

theorem AddSubgroup.zsmul_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {x : G} (hx : x ∈ K) (n : ℤ) : n • x ∈ K

def Subgroup.ofDiv {G : Type u_1} [Group G] (s : Set G) (hsn : s.Nonempty) (hs : ∀ x ∈ s, ∀ y ∈ s, x * y⁻¹ ∈ s) : Subgroup G

Construct a subgroup from a nonempty set that is closed under division.

Equations

• Subgroup.ofDiv s hsn hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

def AddSubgroup.ofSub {G : Type u_1} [AddGroup G] (s : Set G) (hsn : s.Nonempty) (hs : ∀ x ∈ s, ∀ y ∈ s, x + -y ∈ s) : AddSubgroup G

Construct a subgroup from a nonempty set that is closed under subtraction

Equations

• AddSubgroup.ofSub s hsn hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

instance Subgroup.mul {G : Type u_1} [Group G] (H : Subgroup G) : Mul ↥H

A subgroup of a group inherits a multiplication.

Equations

• H.mul = H.mul

instance AddSubgroup.add {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Add ↥H

An AddSubgroup of an AddGroup inherits an addition.

Equations

• H.add = H.add

instance Subgroup.one {G : Type u_1} [Group G] (H : Subgroup G) : One ↥H

A subgroup of a group inherits a 1.

Equations

• H.one = H.one

instance AddSubgroup.zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Zero ↥H

An AddSubgroup of an AddGroup inherits a zero.

Equations

• H.zero = H.zero

instance Subgroup.inv {G : Type u_1} [Group G] (H : Subgroup G) : Inv ↥H

A subgroup of a group inherits an inverse.

Equations

• H.inv = { inv := fun (a : ↥H) => ⟨(↑a)⁻¹, ⋯⟩ }

instance AddSubgroup.neg {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Neg ↥H

An AddSubgroup of an AddGroup inherits an inverse.

Equations

• H.neg = { neg := fun (a : ↥H) => ⟨-↑a, ⋯⟩ }

instance Subgroup.div {G : Type u_1} [Group G] (H : Subgroup G) : Div ↥H

A subgroup of a group inherits a division

Equations

• H.div = { div := fun (a b : ↥H) => ⟨↑a / ↑b, ⋯⟩ }

instance AddSubgroup.sub {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Sub ↥H

An AddSubgroup of an AddGroup inherits a subtraction.

Equations

• H.sub = { sub := fun (a b : ↥H) => ⟨↑a - ↑b, ⋯⟩ }

instance AddSubgroup.nsmul {G : Type u_3} [AddGroup G] {H : AddSubgroup G} : SMul ℕ ↥H

An AddSubgroup of an AddGroup inherits a natural scaling.

Equations

• AddSubgroup.nsmul = { smul := fun (n : ℕ) (a : ↥H) => ⟨n • ↑a, ⋯⟩ }

instance Subgroup.npow {G : Type u_1} [Group G] (H : Subgroup G) : Pow ↥H ℕ

A subgroup of a group inherits a natural power

Equations

• H.npow = { pow := fun (a : ↥H) (n : ℕ) => ⟨↑a ^ n, ⋯⟩ }

instance AddSubgroup.zsmul {G : Type u_3} [AddGroup G] {H : AddSubgroup G} : SMul ℤ ↥H

An AddSubgroup of an AddGroup inherits an integer scaling.

Equations

• AddSubgroup.zsmul = { smul := fun (n : ℤ) (a : ↥H) => ⟨n • ↑a, ⋯⟩ }

instance Subgroup.zpow {G : Type u_1} [Group G] (H : Subgroup G) : Pow ↥H ℤ

A subgroup of a group inherits an integer power

Equations

• H.zpow = { pow := fun (a : ↥H) (n : ℤ) => ⟨↑a ^ n, ⋯⟩ }

@[simp]

theorem Subgroup.coe_mul {G : Type u_1} [Group G] (H : Subgroup G) (x y : ↥H) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem AddSubgroup.coe_add {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x y : ↥H) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem Subgroup.coe_one {G : Type u_1} [Group G] (H : Subgroup G) : ↑1 = 1

@[simp]

theorem AddSubgroup.coe_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ↑0 = 0

@[simp]

theorem Subgroup.coe_inv {G : Type u_1} [Group G] (H : Subgroup G) (x : ↥H) : ↑x⁻¹ = (↑x)⁻¹

@[simp]

theorem AddSubgroup.coe_neg {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : ↥H) : ↑(-x) = -↑x

@[simp]

theorem Subgroup.coe_div {G : Type u_1} [Group G] (H : Subgroup G) (x y : ↥H) : ↑(x / y) = ↑x / ↑y

@[simp]

theorem AddSubgroup.coe_sub {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x y : ↥H) : ↑(x - y) = ↑x - ↑y

theorem Subgroup.coe_mk {G : Type u_1} [Group G] (H : Subgroup G) (x : G) (hx : x ∈ H) : ↑⟨x, hx⟩ = x

theorem AddSubgroup.coe_mk {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : G) (hx : x ∈ H) : ↑⟨x, hx⟩ = x

@[simp]

theorem Subgroup.coe_pow {G : Type u_1} [Group G] (H : Subgroup G) (x : ↥H) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

@[simp]

theorem AddSubgroup.coe_nsmul {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : ↥H) (n : ℕ) : ↑(n • x) = n • ↑x

theorem Subgroup.coe_zpow {G : Type u_1} [Group G] (H : Subgroup G) (x : ↥H) (n : ℤ) : ↑(x ^ n) = ↑x ^ n

theorem AddSubgroup.coe_zsmul {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : ↥H) (n : ℤ) : ↑(n • x) = n • ↑x

@[simp]

theorem Subgroup.mk_eq_one {G : Type u_1} [Group G] (H : Subgroup G) {g : G} {h : g ∈ H} : ⟨g, h⟩ = 1 ↔ g = 1

@[simp]

theorem AddSubgroup.mk_eq_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {g : G} {h : g ∈ H} : ⟨g, h⟩ = 0 ↔ g = 0

instance Subgroup.toGroup {G : Type u_3} [Group G] (H : Subgroup G) : Group ↥H

A subgroup of a group inherits a group structure.

Equations

• H.toGroup = SubgroupClass.toGroup H

instance AddSubgroup.toAddGroup {G : Type u_3} [AddGroup G] (H : AddSubgroup G) : AddGroup ↥H

An AddSubgroup of an AddGroup inherits an AddGroup structure.

Equations

• H.toAddGroup = AddSubgroupClass.toAddGroup H

instance Subgroup.toCommGroup {G : Type u_3} [CommGroup G] (H : Subgroup G) : CommGroup ↥H

A subgroup of a CommGroup is a CommGroup.

Equations

• H.toCommGroup = SubgroupClass.toCommGroup H

instance AddSubgroup.toAddCommGroup {G : Type u_3} [AddCommGroup G] (H : AddSubgroup G) : AddCommGroup ↥H

An AddSubgroup of an AddCommGroup is an AddCommGroup.

Equations

• H.toAddCommGroup = AddSubgroupClass.toAddCommGroup H

def Subgroup.subtype {G : Type u_1} [Group G] (H : Subgroup G) : ↥H →* G

The natural group hom from a subgroup of group G to G.

Equations

• H.subtype = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }

def AddSubgroup.subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ↥H →+ G

The natural group hom from an AddSubgroup of AddGroup G to G.

Equations

• H.subtype = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Subgroup.subtype_apply {G : Type u_1} [Group G] {s : Subgroup G} (x : ↥s) : s.subtype x = ↑x

@[simp]

theorem AddSubgroup.subtype_apply {G : Type u_1} [AddGroup G] {s : AddSubgroup G} (x : ↥s) : s.subtype x = ↑x

theorem Subgroup.subtype_injective {G : Type u_1} [Group G] (s : Subgroup G) : Function.Injective ⇑s.subtype

theorem AddSubgroup.subtype_injective {G : Type u_1} [AddGroup G] (s : AddSubgroup G) : Function.Injective ⇑s.subtype

@[simp]

theorem Subgroup.coe_subtype {G : Type u_1} [Group G] (H : Subgroup G) : ⇑H.subtype = Subtype.val

@[simp]

theorem AddSubgroup.coe_subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⇑H.subtype = Subtype.val

@[deprecated Subgroup.coe_subtype (since := "2025-02-18")]

theorem Subgroup.coeSubtype {G : Type u_1} [Group G] (H : Subgroup G) : ⇑H.subtype = Subtype.val

Alias of Subgroup.coe_subtype.

@[deprecated AddSubgroup.coe_subtype (since := "2025-02-18")]

theorem AddSubgroup.coeSubtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⇑H.subtype = Subtype.val

Alias of AddSubgroup.coe_subtype.

def Subgroup.inclusion {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) : ↥H →* ↥K

The inclusion homomorphism from a subgroup H contained in K to K.

Equations

• Subgroup.inclusion h = MonoidHom.mk' (fun (x : ↥H) => ⟨↑x, ⋯⟩) ⋯

def AddSubgroup.inclusion {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : ↥H →+ ↥K

The inclusion homomorphism from an additive subgroup H contained in K to K.

Equations

• AddSubgroup.inclusion h = AddMonoidHom.mk' (fun (x : ↥H) => ⟨↑x, ⋯⟩) ⋯

@[simp]

theorem Subgroup.coe_inclusion {G : Type u_1} [Group G] {H K : Subgroup G} {h : H ≤ K} (a : ↥H) : ↑((inclusion h) a) = ↑a

@[simp]

theorem AddSubgroup.coe_inclusion {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} {h : H ≤ K} (a : ↥H) : ↑((inclusion h) a) = ↑a

theorem Subgroup.inclusion_injective {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) : Function.Injective ⇑(inclusion h)

theorem AddSubgroup.inclusion_injective {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : Function.Injective ⇑(inclusion h)

@[simp]

theorem Subgroup.inclusion_inj {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) {x y : ↥H} : (inclusion h) x = (inclusion h) y ↔ x = y

@[simp]

theorem AddSubgroup.inclusion_inj {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) {x y : ↥H} : (inclusion h) x = (inclusion h) y ↔ x = y

@[simp]

theorem Subgroup.subtype_comp_inclusion {G : Type u_1} [Group G] {H K : Subgroup G} (hH : H ≤ K) : K.subtype.comp (inclusion hH) = H.subtype

@[simp]

theorem AddSubgroup.subtype_comp_inclusion {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (hH : H ≤ K) : K.subtype.comp (inclusion hH) = H.subtype

class Subgroup.Normal {G : Type u_1} [Group G] (H : Subgroup G) : Prop

A subgroup is normal if whenever n ∈ H, then g * n * g⁻¹ ∈ H for every g : G

• conj_mem (n : G) : n ∈ H → ∀ (g : G), g * n * g⁻¹ ∈ H

  N is closed under conjugation

class AddSubgroup.Normal {A : Type u_2} [AddGroup A] (H : AddSubgroup A) : Prop

An AddSubgroup is normal if whenever n ∈ H, then g + n - g ∈ H for every g : G

• conj_mem (n : A) : n ∈ H → ∀ (g : A), g + n + -g ∈ H

  N is closed under additive conjugation

@[instance 100]

instance Subgroup.normal_of_comm {G : Type u_3} [CommGroup G] (H : Subgroup G) : H.Normal

@[instance 100]

instance AddSubgroup.normal_of_comm {G : Type u_3} [AddCommGroup G] (H : AddSubgroup G) : H.Normal

theorem Subgroup.Normal.conj_mem' {G : Type u_1} [Group G] {H : Subgroup G} (nH : H.Normal) (n : G) (hn : n ∈ H) (g : G) : g⁻¹ * n * g ∈ H

theorem AddSubgroup.Normal.conj_mem' {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (nH : H.Normal) (n : G) (hn : n ∈ H) (g : G) : -g + n + g ∈ H

theorem Subgroup.Normal.mem_comm {G : Type u_1} [Group G] {H : Subgroup G} (nH : H.Normal) {a b : G} (h : a * b ∈ H) : b * a ∈ H

theorem AddSubgroup.Normal.mem_comm {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (nH : H.Normal) {a b : G} (h : a + b ∈ H) : b + a ∈ H

theorem Subgroup.Normal.mem_comm_iff {G : Type u_1} [Group G] {H : Subgroup G} (nH : H.Normal) {a b : G} : a * b ∈ H ↔ b * a ∈ H

theorem AddSubgroup.Normal.mem_comm_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (nH : H.Normal) {a b : G} : a + b ∈ H ↔ b + a ∈ H

def Subgroup.normalizer {G : Type u_1} [Group G] (H : Subgroup G) : Subgroup G

The normalizer of H is the largest subgroup of G inside which H is normal.

Equations

• H.normalizer = { carrier := {g : G | ∀ (n : G), n ∈ H ↔ g * n * g⁻¹ ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

def AddSubgroup.normalizer {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : AddSubgroup G

The normalizer of H is the largest subgroup of G inside which H is normal.

Equations

• H.normalizer = { carrier := {g : G | ∀ (n : G), n ∈ H ↔ g + n + -g ∈ H}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

def Subgroup.setNormalizer {G : Type u_1} [Group G] (S : Set G) : Subgroup G

The setNormalizer of S is the subgroup of G whose elements satisfy g*S*g⁻¹=S

Equations

• Subgroup.setNormalizer S = { carrier := {g : G | ∀ (n : G), n ∈ S ↔ g * n * g⁻¹ ∈ S}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

def AddSubgroup.setNormalizer {G : Type u_1} [AddGroup G] (S : Set G) : AddSubgroup G

The setNormalizer of S is the subgroup of G whose elements satisfy g+S-g=S.

Equations

• AddSubgroup.setNormalizer S = { carrier := {g : G | ∀ (n : G), n ∈ S ↔ g + n + -g ∈ S}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem Subgroup.mem_normalizer_iff {G : Type u_1} [Group G] {H : Subgroup G} {g : G} : g ∈ H.normalizer ↔ ∀ (h : G), h ∈ H ↔ g * h * g⁻¹ ∈ H

theorem AddSubgroup.mem_normalizer_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {g : G} : g ∈ H.normalizer ↔ ∀ (h : G), h ∈ H ↔ g + h + -g ∈ H

theorem Subgroup.mem_normalizer_iff'' {G : Type u_1} [Group G] {H : Subgroup G} {g : G} : g ∈ H.normalizer ↔ ∀ (h : G), h ∈ H ↔ g⁻¹ * h * g ∈ H

theorem AddSubgroup.mem_normalizer_iff'' {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {g : G} : g ∈ H.normalizer ↔ ∀ (h : G), h ∈ H ↔ -g + h + g ∈ H

theorem Subgroup.mem_normalizer_iff' {G : Type u_1} [Group G] {H : Subgroup G} {g : G} : g ∈ H.normalizer ↔ ∀ (n : G), n * g ∈ H ↔ g * n ∈ H

theorem AddSubgroup.mem_normalizer_iff' {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {g : G} : g ∈ H.normalizer ↔ ∀ (n : G), n + g ∈ H ↔ g + n ∈ H

theorem Subgroup.le_normalizer {G : Type u_1} [Group G] {H : Subgroup G} : H ≤ H.normalizer

theorem AddSubgroup.le_normalizer {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H ≤ H.normalizer

@[deprecated IsMulCommutative (since := "2025-04-09")]

def Subgroup.IsCommutative (M : Type u_2) [Mul M] : Prop

Alias of IsMulCommutative.

---

A Prop stating that the multiplication is commutative.

Equations

• Subgroup.IsCommutative = IsMulCommutative

@[deprecated IsAddCommutative (since := "2025-04-09")]

def AddSubgroup.IsCommutative (M : Type u_2) [Add M] : Prop

Alias of IsAddCommutative.

---

A Prop stating that the addition is commutative.

Equations

• AddSubgroup.IsCommutative = IsAddCommutative

instance Subgroup.commGroup_isMulCommutative {G : Type u_3} [CommGroup G] (H : Subgroup G) : IsMulCommutative ↥H

A subgroup of a commutative group is commutative.

instance AddSubgroup.addCommGroup_isAddCommutative {G : Type u_3} [AddCommGroup G] (H : AddSubgroup G) : IsAddCommutative ↥H

A subgroup of a commutative group is commutative.

@[deprecated Subgroup.commGroup_isMulCommutative (since := "2025-04-09")]

theorem Subgroup.commGroup_isCommutative {G : Type u_3} [CommGroup G] (H : Subgroup G) : IsMulCommutative ↥H

Alias of Subgroup.commGroup_isMulCommutative.

---

A subgroup of a commutative group is commutative.

@[deprecated Subgroup.commGroup_isMulCommutative (since := "2025-04-09")]

theorem AddSubgroup.addCommGroup_isCommutative {G : Type u_3} [CommGroup G] (H : Subgroup G) : IsMulCommutative ↥H

Alias of Subgroup.commGroup_isMulCommutative.

---

A subgroup of a commutative group is commutative.

theorem Subgroup.mul_comm_of_mem_isMulCommutative {G : Type u_1} [Group G] (H : Subgroup G) [IsMulCommutative ↥H] {a b : G} (ha : a ∈ H) (hb : b ∈ H) : a * b = b * a

theorem AddSubgroup.add_comm_of_mem_isAddCommutative {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [IsAddCommutative ↥H] {a b : G} (ha : a ∈ H) (hb : b ∈ H) : a + b = b + a

@[deprecated Subgroup.mul_comm_of_mem_isMulCommutative (since := "2025-04-09")]

theorem Subgroup.mul_comm_of_mem_isCommutative {G : Type u_1} [Group G] (H : Subgroup G) [IsMulCommutative ↥H] {a b : G} (ha : a ∈ H) (hb : b ∈ H) : a * b = b * a

Alias of Subgroup.mul_comm_of_mem_isMulCommutative.

@[deprecated AddSubgroup.add_comm_of_mem_isAddCommutative (since := "2025-04-09")]

theorem AddSubgroup.add_comm_of_mem_isCommutative {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [IsAddCommutative ↥H] {a b : G} (ha : a ∈ H) (hb : b ∈ H) : a + b = b + a

Alias of AddSubgroup.add_comm_of_mem_isAddCommutative.