Subgroups

This file defines multiplicative and additive subgroups as an extension of submonoids, in a bundled form.

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 HasMemOrNegMem {S : Type u_3} {G : Type u_4} [Neg G] [SetLike S G] (s : S) : Prop

Typeclass for substructures s such that s ∪ -s = G.

• mem_or_neg_mem (a : G) : a ∈ s ∨ -a ∈ s

class HasMemOrInvMem {S : Type u_3} {G : Type u_4} [Inv G] [SetLike S G] (s : S) : Prop

Typeclass for substructures s such that s ∪ s⁻¹ = G.

• mem_or_inv_mem (a : G) : a ∈ s ∨ a⁻¹ ∈ s

theorem HasMemOrInvMem.inv_mem_of_notMem {S : Type u_3} {G : Type u_4} [Inv G] [SetLike S G] (s : S) [HasMemOrInvMem s] (x : G) (h : ¬x ∈ s) : x⁻¹ ∈ s

theorem HasMemOrNegMem.neg_mem_of_notMem {S : Type u_3} {G : Type u_4} [Neg G] [SetLike S G] (s : S) [HasMemOrNegMem s] (x : G) (h : ¬x ∈ s) : -x ∈ s

theorem HasMemOrInvMem.mem_of_inv_notMem {S : Type u_3} {G : Type u_4} [Inv G] [SetLike S G] (s : S) [HasMemOrInvMem s] (x : G) (h : ¬x⁻¹ ∈ s) : x ∈ s

theorem HasMemOrNegMem.mem_of_neg_notMem {S : Type u_3} {G : Type u_4} [Neg G] [SetLike S G] (s : S) [HasMemOrNegMem s] (x : G) (h : ¬-x ∈ s) : x ∈ s

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 : G), x ∈ H ∧ P x⁻¹) ↔ ∃ (x : G), 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 : G), x ∈ H ∧ P (-x)) ↔ ∃ (x : G), 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_5} {S : Type u_6} [Inv G] [SetLike S G] [InvMemClass S G] {H : S} : Inv ↥H

A subgroup of a group inherits an inverse.

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

An additive subgroup of an AddGroup inherits an inverse.

@[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] [LE S] [IsConcreteLE 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] [LE S] [IsConcreteLE S G] {H K L : S} : ↑H ⊆ ↑K ∪ ↑L ↔ H ≤ K ∨ H ≤ L

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

A subgroup of a group inherits a division

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

An additive subgroup of an AddGroup inherits a subtraction.

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.

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.

@[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.

@[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.

@[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.

@[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.

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.

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.

@[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

@[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] [LE S] [IsConcreteLE S G] {H K : S} (h : H ≤ K) : ↥H →* ↥K

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

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

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

@[simp]

theorem SubgroupClass.inclusion_self {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] [Preorder S] [IsConcreteLE 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] [Preorder S] [IsConcreteLE 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] [LE S] [IsConcreteLE 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] [LE S] [IsConcreteLE 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] [LE S] [IsConcreteLE 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] [LE S] [IsConcreteLE 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] [Preorder S] [IsConcreteLE 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] [LE S] [IsConcreteLE 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] [LE S] [IsConcreteLE 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] [LE S] [IsConcreteLE S G] {H K : S} (h : H ≤ K) : (↑K).comp (inclusion h) = ↑H

@[simp]

theorem AddSubgroupClass.subtype_comp_inclusion {G : Type u_1} [AddGroup G] {S : Type u_4} [SetLike S G] [AddSubgroupClass S G] [LE S] [IsConcreteLE S G] {H K : S} (h : H ≤ K) : (↑K).comp (inclusion h) = ↑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

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

instance Subgroup.instPartialOrder {G : Type u_1} [Group G] : PartialOrder (Subgroup G)

instance AddSubgroup.instPartialOrder {G : Type u_1} [AddGroup G] : PartialOrder (AddSubgroup G)

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

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

@[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

@[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

@[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 : Submonoid G} {x : G} (h_inv : ∀ {x : G}, x ∈ s.carrier → x⁻¹ ∈ s.carrier) : x ∈ { toSubmonoid := s, inv_mem' := h_inv } ↔ x ∈ s

@[simp]

theorem AddSubgroup.mem_mk {G : Type u_1} [AddGroup G] {s : AddSubmonoid G} {x : G} (h_neg : ∀ {x : G}, x ∈ s.carrier → -x ∈ s.carrier) : x ∈ { toAddSubmonoid := s, neg_mem' := h_neg } ↔ x ∈ s

@[simp]

theorem Subgroup.coe_set_mk {G : Type u_1} [Group G] {s : Submonoid G} (h_inv : ∀ {x : G}, x ∈ s.carrier → x⁻¹ ∈ s.carrier) : ↑{ toSubmonoid := s, inv_mem' := h_inv } = ↑s

@[simp]

theorem AddSubgroup.coe_set_mk {G : Type u_1} [AddGroup G] {s : AddSubmonoid G} (h_neg : ∀ {x : G}, x ∈ s.carrier → -x ∈ s.carrier) : ↑{ toAddSubmonoid := s, neg_mem' := h_neg } = ↑s

@[simp]

theorem Subgroup.mk_le_mk {G : Type u_1} [Group G] {s t : Submonoid G} (h_inv : ∀ {x : G}, x ∈ s.carrier → x⁻¹ ∈ s.carrier) (h_inv' : ∀ {x : G}, x ∈ t.carrier → x⁻¹ ∈ t.carrier) : { toSubmonoid := s, inv_mem' := h_inv } ≤ { toSubmonoid := t, inv_mem' := h_inv' } ↔ s ≤ t

@[simp]

theorem AddSubgroup.mk_le_mk {G : Type u_1} [AddGroup G] {s t : AddSubmonoid G} (h_neg : ∀ {x : G}, x ∈ s.carrier → -x ∈ s.carrier) (h_neg' : ∀ {x : G}, x ∈ t.carrier → -x ∈ t.carrier) : { toAddSubmonoid := s, neg_mem' := h_neg } ≤ { toAddSubmonoid := t, neg_mem' := h_neg' } ↔ 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

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.

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

@[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 Subgroup.ext_iff {G : Type u_1} [Group G] {H K : Subgroup G} : H = K ↔ ∀ (x : G), x ∈ H ↔ x ∈ K

theorem AddSubgroup.ext_iff {G : Type u_1} [AddGroup G] {H K : AddSubgroup 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 : G), x ∈ K ∧ P x⁻¹) ↔ ∃ (x : G), 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 : G), x ∈ K ∧ P (-x)) ↔ ∃ (x : G), 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 : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s) : Subgroup G

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

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

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

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

A subgroup of a group inherits a multiplication.

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

An AddSubgroup of an AddGroup inherits an addition.

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

A subgroup of a group inherits a 1.

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

An AddSubgroup of an AddGroup inherits a zero.

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

A subgroup of a group inherits an inverse.

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

An AddSubgroup of an AddGroup inherits an inverse.

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

A subgroup of a group inherits a division

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

An AddSubgroup of an AddGroup inherits a subtraction.

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

An AddSubgroup of an AddGroup inherits a natural scaling.

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

A subgroup of a group inherits a natural power

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

An AddSubgroup of an AddGroup inherits an integer scaling.

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

A subgroup of a group inherits an integer power

@[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.

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

An AddSubgroup of an AddGroup inherits an AddGroup structure.

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

A subgroup of a CommGroup is a CommGroup.

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

An AddSubgroup of an AddCommGroup is an AddCommGroup.

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.

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.

@[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

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.

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.

@[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 H 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

  H is closed under conjugation

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

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

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

  H 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.

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.

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

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.

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

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.

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

theorem Set.injOn_iff_map_eq_one {F : Type u_3} {G : Type u_4} {H : Type u_5} {S : Type u_6} [Group G] [Group H] [FunLike F G H] [MonoidHomClass F G H] (f : F) [SetLike S G] [OneMemClass S G] [MulMemClass S G] [InvMemClass S G] (s : S) : InjOn ⇑f ↑s ↔ ∀ (a : G), a ∈ s → f a = 1 → a = 1

theorem Set.injOn_iff_map_eq_zero {F : Type u_3} {G : Type u_4} {H : Type u_5} {S : Type u_6} [AddGroup G] [AddGroup H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) [SetLike S G] [ZeroMemClass S G] [AddMemClass S G] [NegMemClass S G] (s : S) : InjOn ⇑f ↑s ↔ ∀ (a : G), a ∈ s → f a = 0 → a = 0