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_5) (G : outParam (Type u_6)) [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

theorem InvMemClass.inv_mem {S : Type u_5} {G : outParam (Type u_6)} : ∀ {inst : Inv G} {inst_1 : SetLike S G} [self : InvMemClass S G] {s : S} {x : G}, x ∈ s → x⁻¹ ∈ s

s is closed under inverses

class NegMemClass (S : Type u_5) (G : outParam (Type u_6)) [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

theorem NegMemClass.neg_mem {S : Type u_5} {G : outParam (Type u_6)} : ∀ {inst : Neg G} {inst_1 : SetLike S G} [self : NegMemClass S G] {s : S} {x : G}, x ∈ s → -x ∈ s

s is closed under negation

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

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

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

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

@[simp]

theorem neg_mem_iff {S : Type u_5} {G : Type u_6} [InvolutiveNeg G] : ∀ {x : SetLike S G} [inst : NegMemClass S G] {H : S} {x_1 : G}, -x_1 ∈ H ↔ x_1 ∈ H

@[simp]

theorem inv_mem_iff {S : Type u_5} {G : Type u_6} [InvolutiveInv G] : ∀ {x : SetLike S G} [inst : InvMemClass S G] {H : S} {x_1 : G}, x_1⁻¹ ∈ H ↔ x_1 ∈ H

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

An additive subgroup is closed under subtraction.

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

A subgroup is closed under division.

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

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

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

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

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

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

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

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

theorem NegMemClass.neg.proof_1 {G : Type u_1} {S : Type u_2} [Neg G] [SetLike S G] [NegMemClass S G] {H : S} (a : ↥H) : -↑a ∈ H

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, ⋯⟩ }

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)⁻¹, ⋯⟩ }

@[simp]

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

@[simp]

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

@[deprecated]

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

Alias of InvMemClass.coe_inv.

@[deprecated]

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

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

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

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, ⋯⟩ }

theorem AddSubgroupClass.sub.proof_1 {G : Type u_1} {S : Type u_2} [SubNegMonoid G] [SetLike S G] [AddSubgroupClass S G] {H : S} (a : ↥H) (b : ↥H) : ↑a - ↑b ∈ H

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.zsmul {M : Type u_7} {S : Type u_8} [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_7} {S : Type u_8} [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 AddSubgroupClass.coe_sub {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : ↥H) (y : ↥H) : ↑(x - y) = ↑x - ↑y

@[simp]

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

theorem AddSubgroupClass.toAddGroup.proof_1 {G : Type u_2} [AddGroup G] {S : Type u_1} [SetLike S G] [AddSubgroupClass S G] : AddSubmonoidClass S G

theorem AddSubgroupClass.toAddGroup.proof_5 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] : ↑0 = ↑0

theorem AddSubgroupClass.toAddGroup.proof_4 {G : Type u_1} {S : Type u_2} (H : S) [SetLike S G] : Function.Injective fun (a : ↥H) => ↑a

theorem AddSubgroupClass.toAddGroup.proof_6 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] : ∀ (x x_1 : ↥H), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubgroupClass.toAddGroup.proof_9 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] : ∀ (x : ↥H) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubgroupClass.toAddGroup.proof_10 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] : ∀ (x : ↥H) (x_1 : ℤ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubgroupClass.toAddGroup.proof_7 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] : ∀ (x : ↥H), ↑(-x) = ↑(-x)

theorem AddSubgroupClass.toAddGroup.proof_3 {G : Type u_2} [AddGroup G] {S : Type u_1} [SetLike S G] [AddSubgroupClass S G] : NegMemClass S G

@[instance 75]

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

An additive subgroup of an AddGroup inherits an AddGroup structure.

Equations

• AddSubgroupClass.toAddGroup H = Function.Injective.addGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubgroupClass.toAddGroup.proof_8 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] : ∀ (x x_1 : ↥H), ↑(x - x_1) = ↑(x - x_1)

theorem AddSubgroupClass.toAddGroup.proof_2 {G : Type u_2} [AddGroup G] {S : Type u_1} [SetLike S G] [AddSubgroupClass S G] : ZeroMemClass S G

@[instance 75]

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

A subgroup of a group inherits a group structure.

Equations

• SubgroupClass.toGroup H = Function.Injective.group (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubgroupClass.toAddCommGroup.proof_10 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x : ↥H) (x_1 : ℤ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubgroupClass.toAddCommGroup.proof_7 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x : ↥H), ↑(-x) = ↑(-x)

theorem AddSubgroupClass.toAddCommGroup.proof_6 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x x_1 : ↥H), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubgroupClass.toAddCommGroup.proof_9 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x : ↥H) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubgroupClass.toAddCommGroup.proof_5 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ↑0 = ↑0

theorem AddSubgroupClass.toAddCommGroup.proof_4 {S : Type u_2} (H : S) {G : Type u_1} [SetLike S G] : Function.Injective fun (a : ↥H) => ↑a

theorem AddSubgroupClass.toAddCommGroup.proof_1 {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ZeroMemClass S G

theorem AddSubgroupClass.toAddCommGroup.proof_3 {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : NegMemClass S G

theorem AddSubgroupClass.toAddCommGroup.proof_2 {S : Type u_1} {G : Type u_2} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : AddSubmonoidClass S G

@[instance 75]

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

An additive subgroup of an AddCommGroup is an AddCommGroup.

Equations

• AddSubgroupClass.toAddCommGroup H = Function.Injective.addCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubgroupClass.toAddCommGroup.proof_8 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x x_1 : ↥H), ↑(x - x_1) = ↑(x - x_1)

@[instance 75]

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

A subgroup of a CommGroup is a CommGroup.

Equations

• SubgroupClass.toCommGroup H = Function.Injective.commGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubgroupClass.subtype.proof_2 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] : ∀ (x x_1 : ↥H), { toFun := Subtype.val, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := Subtype.val, map_zero' := ⋯ }.toFun (x + x_1)

theorem AddSubgroupClass.subtype.proof_1 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] : ↑0 = ↑0

def AddSubgroupClass.subtype {G : Type u_1} [AddGroup G] {S : Type u_6} (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' := ⋯ }

def SubgroupClass.subtype {G : Type u_1} [Group G] {S : Type u_6} (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' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem SubgroupClass.coe_pow {G : Type u_1} [Group G] {S : Type u_6} {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_6} {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_6} {H : S} [SetLike S G] [SubgroupClass S G] (x : ↥H) (n : ℤ) : ↑(x ^ n) = ↑x ^ n

theorem AddSubgroupClass.inclusion.proof_1 {G : Type u_1} {S : Type u_2} [SetLike S G] {H : S} {K : S} (h : H ≤ K) (x : ↥H) : ↑x ∈ K

def AddSubgroupClass.inclusion {G : Type u_1} [AddGroup G] {S : Type u_6} [SetLike S G] [AddSubgroupClass S G] {H : S} {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, ⋯⟩) ⋯

theorem AddSubgroupClass.inclusion.proof_2 {G : Type u_1} [AddGroup G] {S : Type u_2} [SetLike S G] [AddSubgroupClass S G] {H : S} {K : S} (h : H ≤ K) : ∀ (x x_1 : ↥H), (fun (x : ↥H) => ⟨↑x, ⋯⟩) (x + x_1) = (fun (x : ↥H) => ⟨↑x, ⋯⟩) (x + x_1)

def SubgroupClass.inclusion {G : Type u_1} [Group G] {S : Type u_6} [SetLike S G] [SubgroupClass S G] {H : S} {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, ⋯⟩) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem Subgroup.inv_mem' {G : Type u_5} [Group G] (self : Subgroup G) {x : G} : x ∈ self.carrier → x⁻¹ ∈ self.carrier

G is closed under inverses

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

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

theorem AddSubgroup.neg_mem' {G : Type u_5} [AddGroup G] (self : AddSubgroup G) {x : G} : x ∈ self.carrier → -x ∈ self.carrier

G is closed under negation

theorem AddSubgroup.instSetLike.proof_1 {G : Type u_1} [AddGroup G] (p : AddSubgroup G) (q : AddSubgroup G) (h : (fun (s : AddSubgroup G) => s.carrier) p = (fun (s : AddSubgroup G) => s.carrier) q) : p = q

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' := ⋯ }

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.instAddSubgroupClass {G : Type u_1} [AddGroup G] : AddSubgroupClass (AddSubgroup G) G

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

theorem Subgroup.mem_carrier {G : Type u_1} [Group G] {s : Subgroup G} {x : G} : x ∈ s.carrier ↔ 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.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.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.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.mk_le_mk {G : Type u_1} [AddGroup G] {s : Set G} {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.mk_le_mk {G : Type u_1} [Group G] {s : Set G} {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.coe_toAddSubmonoid {G : Type u_1} [AddGroup G] (K : AddSubgroup G) : ↑K.toAddSubmonoid = ↑K

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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' := ⋯ }

theorem AddSubgroup.copy.proof_1 {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = ↑K) : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s

theorem AddSubgroup.copy.proof_3 {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = ↑K) : ∀ {x : G}, x ∈ { carrier := s, add_mem' := ⋯, zero_mem' := ⋯ }.carrier → -x ∈ { carrier := s, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

theorem AddSubgroup.copy.proof_2 {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = ↑K) : 0 ∈ { carrier := s, add_mem' := ⋯ }.carrier

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' := ⋯ }

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

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

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.copy_eq {G : Type u_1} [Group G] (K : Subgroup G) (s : Set G) (hs : s = ↑K) : K.copy s hs = K

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

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

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

Two subgroups are equal if they have the same elements.

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

An AddSubgroup contains the group's 0.

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

A subgroup contains the group's 1.

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

An AddSubgroup is closed under addition.

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

A subgroup is closed under multiplication.

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.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.sub_mem {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x : G} {y : G} (hx : x ∈ H) (hy : y ∈ H) : x - y ∈ H

An AddSubgroup is closed under subtraction.

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

A subgroup is closed under division.

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

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

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.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.add_mem_cancel_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x : G} {y : G} (h : x ∈ H) : y + x ∈ H ↔ y ∈ H

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

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

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

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

theorem Subgroup.pow_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

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

theorem AddSubgroup.ofSub.proof_3 {G : Type u_1} [AddGroup G] (s : Set G) (hs : ∀ x ∈ s, ∀ y ∈ s, x + -y ∈ s) (inv_mem : ∀ x ∈ s, -x ∈ s) : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s

theorem AddSubgroup.ofSub.proof_2 {G : Type u_1} [AddGroup G] (s : Set G) (hs : ∀ x ∈ s, ∀ y ∈ s, x + -y ∈ s) (one_mem : 0 ∈ s) (x : G) (hx : x ∈ s) : -x ∈ s

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' := ⋯ }

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

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' := ⋯ }

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

theorem AddSubgroup.neg.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (a : ↥H) : -↑a ∈ H

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.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)⁻¹, ⋯⟩ }

theorem AddSubgroup.sub.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (a : ↥H) (b : ↥H) : ↑a - ↑b ∈ H

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 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.nsmul {G : Type u_5} [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_5} [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 AddSubgroup.coe_add {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : ↥H) (y : ↥H) : ↑(x + y) = ↑x + ↑y

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem Subgroup.coe_pow {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

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

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

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

theorem AddSubgroup.toAddGroup.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Function.Injective fun (a : ↥H) => ↑a

theorem AddSubgroup.toAddGroup.proof_7 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ∀ (x : ↥H) (x_1 : ℤ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubgroup.toAddGroup.proof_5 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ∀ (x x_1 : ↥H), ↑(x - x_1) = ↑(x - x_1)

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

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

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

An AddSubgroup of an AddGroup inherits an AddGroup structure.

Equations

• H.toAddGroup = Function.Injective.addGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubgroup.toAddGroup.proof_3 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ∀ (x x_1 : ↥H), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubgroup.toAddGroup.proof_6 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ∀ (x : ↥H) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

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

A subgroup of a group inherits a group structure.

Equations

• H.toGroup = Function.Injective.group (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubgroup.toAddCommGroup.proof_5 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) : ∀ (x x_1 : ↥H), ↑(x - x_1) = ↑(x - x_1)

theorem AddSubgroup.toAddCommGroup.proof_1 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) : Function.Injective fun (a : ↥H) => ↑a

theorem AddSubgroup.toAddCommGroup.proof_4 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) : ∀ (x : ↥H), ↑(-x) = ↑(-x)

theorem AddSubgroup.toAddCommGroup.proof_3 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) : ∀ (x x_1 : ↥H), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubgroup.toAddCommGroup.proof_2 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) : ↑0 = ↑0

theorem AddSubgroup.toAddCommGroup.proof_7 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) : ∀ (x : ↥H) (x_1 : ℤ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubgroup.toAddCommGroup.proof_6 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) : ∀ (x : ↥H) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

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

An AddSubgroup of an AddCommGroup is an AddCommGroup.

Equations

• H.toAddCommGroup = Function.Injective.addCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

A subgroup of a CommGroup is a CommGroup.

Equations

• H.toCommGroup = Function.Injective.commGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

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' := ⋯ }

theorem AddSubgroup.subtype.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ∀ (x x_1 : ↥H), { toFun := Subtype.val, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := Subtype.val, map_zero' := ⋯ }.toFun (x + x_1)

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' := ⋯ }

@[simp]

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

@[simp]

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

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

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

theorem AddSubgroup.inclusion.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) (x : ↥H) : ↑x ∈ K

theorem AddSubgroup.inclusion.proof_2 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) : ∀ (x x_1 : ↥H), (fun (x : ↥H) => ⟨↑x, ⋯⟩) (x + x_1) = (fun (x : ↥H) => ⟨↑x, ⋯⟩) (x + x_1)

def AddSubgroup.inclusion {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {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, ⋯⟩) ⋯

def Subgroup.inclusion {G : Type u_1} [Group G] {H : Subgroup G} {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, ⋯⟩) ⋯

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Subgroup.subtype_comp_inclusion {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hH : H ≤ K) : K.subtype.comp (Subgroup.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 ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H

  N is closed under conjugation

theorem Subgroup.Normal.conj_mem {G : Type u_1} [Group G] {H : Subgroup G} (self : H.Normal) (n : G) : n ∈ H → ∀ (g : G), g * n * g⁻¹ ∈ H

N is closed under conjugation

class AddSubgroup.Normal {A : Type u_4} [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 ∈ H, ∀ (g : A), g + n + -g ∈ H

  N is closed under additive conjugation

theorem AddSubgroup.Normal.conj_mem {A : Type u_4} [AddGroup A] {H : AddSubgroup A} (self : H.Normal) (n : A) : n ∈ H → ∀ (g : A), g + n + -g ∈ H

N is closed under additive conjugation

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

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.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.mem_comm {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (nH : H.Normal) {a : G} {b : G} (h : a + b ∈ H) : b + a ∈ H

theorem Subgroup.Normal.mem_comm {G : Type u_1} [Group G] {H : Subgroup G} (nH : H.Normal) {a : G} {b : G} (h : 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 : G} {b : G} : 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 : G} {b : G} : a * b ∈ H ↔ b * a ∈ H

theorem AddSubgroup.normalizer.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (a : G) : a ∈ H ↔ 0 + a + -0 ∈ H

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' := ⋯ }

theorem AddSubgroup.normalizer.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {a : G} {b : G} (ha : ∀ (n : G), n ∈ H ↔ a + n + -a ∈ H) (hb : ∀ (n : G), n ∈ H ↔ b + n + -b ∈ H) (n : G) : n ∈ H ↔ a + b + n + -(a + b) ∈ H

theorem AddSubgroup.normalizer.proof_3 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {a : G} (ha : ∀ (n : G), n ∈ H ↔ a + n + -a ∈ H) (n : G) : n ∈ H ↔ -a + n + - -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' := ⋯ }

theorem AddSubgroup.setNormalizer.proof_1 {G : Type u_1} [AddGroup G] (S : Set G) {a : G} {b : G} (ha : ∀ (n : G), n ∈ S ↔ a + n + -a ∈ S) (hb : ∀ (n : G), n ∈ S ↔ b + n + -b ∈ S) (n : G) : n ∈ S ↔ a + b + n + -(a + b) ∈ S

theorem AddSubgroup.setNormalizer.proof_2 {G : Type u_1} [AddGroup G] (S : Set G) (a : G) : a ∈ S ↔ 0 + a + -0 ∈ 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.

Equations

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

theorem AddSubgroup.setNormalizer.proof_3 {G : Type u_1} [AddGroup G] (S : Set G) {a : G} (ha : ∀ (n : G), n ∈ S ↔ a + n + -a ∈ S) (n : G) : n ∈ S ↔ -a + n + - -a ∈ S

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' := ⋯ }

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 ↔ ∀ (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 ↔ ∀ (n : G), n + g ∈ H ↔ g + n ∈ 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.le_normalizer {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H ≤ H.normalizer

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

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

Commutativity of a subgroup

• is_comm : Std.Commutative fun (x1 x2 : ↥H) => x1 * x2

  * is commutative on H

theorem Subgroup.IsCommutative.is_comm {G : Type u_1} [Group G] {H : Subgroup G} (self : H.IsCommutative) : Std.Commutative fun (x1 x2 : ↥H) => x1 * x2

* is commutative on H

class AddSubgroup.IsCommutative {A : Type u_4} [AddGroup A] (H : AddSubgroup A) : Prop

Commutativity of an additive subgroup

• is_comm : Std.Commutative fun (x1 x2 : ↥H) => x1 + x2

  + is commutative on H

theorem AddSubgroup.IsCommutative.is_comm {A : Type u_4} [AddGroup A] {H : AddSubgroup A} (self : H.IsCommutative) : Std.Commutative fun (x1 x2 : ↥H) => x1 + x2

+ is commutative on H

theorem AddSubgroup.IsCommutative.addCommGroup.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [h : H.IsCommutative] (a : ↥H) (b : ↥H) : a + b = b + a

instance AddSubgroup.IsCommutative.addCommGroup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [h : H.IsCommutative] : AddCommGroup ↥H

A commutative subgroup is commutative.

Equations

• AddSubgroup.IsCommutative.addCommGroup H = AddCommGroup.mk ⋯

instance Subgroup.IsCommutative.commGroup {G : Type u_1} [Group G] (H : Subgroup G) [h : H.IsCommutative] : CommGroup ↥H

A commutative subgroup is commutative.

Equations

• Subgroup.IsCommutative.commGroup H = CommGroup.mk ⋯

instance AddSubgroup.addCommGroup_isCommutative {G : Type u_5} [AddCommGroup G] (H : AddSubgroup G) : H.IsCommutative

A subgroup of a commutative group is commutative.

Equations

• ⋯ = ⋯

instance Subgroup.commGroup_isCommutative {G : Type u_5} [CommGroup G] (H : Subgroup G) : H.IsCommutative

A subgroup of a commutative group is commutative.

Equations

• ⋯ = ⋯

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

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