Subgroups

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

We prove subgroups of a group form a complete lattice, and results about images and preimages of subgroups under group homomorphisms. The bundled subgroups use bundled monoid homomorphisms.

There are also theorems about the subgroups generated by an element or a subset of a group, defined both inductively and as the infimum of the set of subgroups containing a given element/subset.

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

• CompleteLattice (Subgroup G) : the subgroups of G form a complete lattice

• Subgroup.closure k : the minimal subgroup that includes the set k

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

• Subgroup.gi : closure forms a Galois insertion with the coercion to set

• Subgroup.comap H f : the preimage of a subgroup H along the group homomorphism f is also a subgroup

• Subgroup.map f H : the image of a subgroup H along the group homomorphism f is also a subgroup

• Subgroup.prod H K : the product of subgroups H, K of groups G, N respectively, H × K is a subgroup of G × N

• MonoidHom.range f : the range of the group homomorphism f is a subgroup

• MonoidHom.ker f : the kernel of a group homomorphism f is the subgroup of elements x : G such that f x = 1

• MonoidHom.eq_locus f g : given group homomorphisms f, g, the elements of G such that f x = g x form a subgroup of 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 : Type u_6) [Inv G] [SetLike S G] : Prop

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

  s is closed under inverses

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

class NegMemClass (S : Type u_5) (G : Type u_6) [Neg G] [SetLike S G] : Prop

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

  s is closed under negation

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

class SubgroupClass (S : Type u_5) (G : 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 : 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

@[simp]

theorem abs_mem_iff {S : Type u_5} {G : Type u_6} [InvolutiveNeg G] [LinearOrder G] : ∀ {x : SetLike S G} [inst : NegMemClass 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.

abbrev zsmul_mem.match_1 (motive : ℤ → Prop) : (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x

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 sub_mem_comm_iff {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] {a : G} {b : G} : a - b ∈ H ↔ b - a ∈ H

theorem div_mem_comm_iff {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] {a : G} {b : G} : a / b ∈ H ↔ b / a ∈ H

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, x ∈ H ∧ P (-x)) ↔ ∃ 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, x ∈ H ∧ P x⁻¹) ↔ ∃ 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 AddSubgroupClass.neg.proof_1 {G : Type u_1} {S : Type u_2} [SubNegMonoid G] [SetLike S G] [AddSubgroupClass S G] {H : S} (a : { x // x ∈ H }) : -↑a ∈ H

instance AddSubgroupClass.neg {G : Type u_1} {S : Type u_2} [SubNegMonoid G] [SetLike S G] [AddSubgroupClass S G] {H : S} : Neg { x // x ∈ H }

An additive subgroup of an AddGroup inherits an inverse.

instance SubgroupClass.inv {G : Type u_1} {S : Type u_2} [DivInvMonoid G] [SetLike S G] [SubgroupClass S G] {H : S} : Inv { x // x ∈ H }

A subgroup of a group inherits an inverse.

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

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

An additive subgroup of an AddGroup inherits a subtraction.

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

A subgroup of a group inherits a division

instance AddSubgroupClass.zsmul {M : Type u_7} {S : Type u_8} [SubNegMonoid M] [SetLike S M] [AddSubgroupClass S M] {H : S} : SMul ℤ { x // x ∈ H }

An additive subgroup of an AddGroup inherits an integer scaling.

instance SubgroupClass.zpow {M : Type u_7} {S : Type u_8} [DivInvMonoid M] [SetLike S M] [SubgroupClass S M] {H : S} : Pow { x // x ∈ H } ℤ

A subgroup of a group inherits an integer power.

@[simp]

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

@[simp]

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

@[simp]

theorem AddSubgroupClass.coe_sub {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : { x // x ∈ H }) (y : { x // x ∈ 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 : { x // x ∈ H }) (y : { x // x ∈ H }) : ↑(x / y) = ↑x / ↑y

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

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 // x ∈ H }), ↑(-x) = ↑(-x)

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

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

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

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

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

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

An additive subgroup of an AddGroup inherits an AddGroup structure.

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

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 // x ∈ H }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

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

A subgroup of a group inherits a group structure.

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

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

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

An additive subgroup of an AddCommGroup is an AddCommGroup.

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

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 // x ∈ H }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

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

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 // x ∈ H }), ↑(-x) = ↑(-x)

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

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

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

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

A subgroup of a CommGroup is a CommGroup.

theorem AddSubgroupClass.toOrderedAddCommGroup.proof_8 {S : Type u_2} (H : S) {G : Type u_1} [OrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x : { x // x ∈ H }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubgroupClass.toOrderedAddCommGroup.proof_9 {S : Type u_2} (H : S) {G : Type u_1} [OrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x : { x // x ∈ H }) (x_1 : ℤ), ↑(x_1 • x) = ↑(x_1 • x)

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

theorem AddSubgroupClass.toOrderedAddCommGroup.proof_7 {S : Type u_2} (H : S) {G : Type u_1} [OrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x x_1 : { x // x ∈ H }), ↑(x - x_1) = ↑(x - x_1)

theorem AddSubgroupClass.toOrderedAddCommGroup.proof_5 {S : Type u_2} (H : S) {G : Type u_1} [OrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x x_1 : { x // x ∈ H }), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubgroupClass.toOrderedAddCommGroup.proof_4 {S : Type u_2} (H : S) {G : Type u_1} [OrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ↑0 = ↑0

theorem AddSubgroupClass.toOrderedAddCommGroup.proof_6 {S : Type u_2} (H : S) {G : Type u_1} [OrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x : { x // x ∈ H }), ↑(-x) = ↑(-x)

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

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

instance AddSubgroupClass.toOrderedAddCommGroup {S : Type u_6} (H : S) {G : Type u_7} [OrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : OrderedAddCommGroup { x // x ∈ H }

An additive subgroup of an AddOrderedCommGroup is an AddOrderedCommGroup.

instance SubgroupClass.toOrderedCommGroup {S : Type u_6} (H : S) {G : Type u_7} [OrderedCommGroup G] [SetLike S G] [SubgroupClass S G] : OrderedCommGroup { x // x ∈ H }

A subgroup of an OrderedCommGroup is an OrderedCommGroup.

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

theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_4 {S : Type u_2} (H : S) {G : Type u_1} [LinearOrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ↑0 = ↑0

theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_5 {S : Type u_2} (H : S) {G : Type u_1} [LinearOrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x x_1 : { x // x ∈ H }), ↑(x + x_1) = ↑(x + x_1)

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

instance AddSubgroupClass.toLinearOrderedAddCommGroup {S : Type u_6} (H : S) {G : Type u_7} [LinearOrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : LinearOrderedAddCommGroup { x // x ∈ H }

An additive subgroup of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_11 {S : Type u_2} (H : S) {G : Type u_1} [LinearOrderedAddCommGroup G] [SetLike S G] : ∀ (x x_1 : { x // x ∈ H }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_9 {S : Type u_2} (H : S) {G : Type u_1} [LinearOrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x : { x // x ∈ H }) (x_1 : ℤ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_7 {S : Type u_2} (H : S) {G : Type u_1} [LinearOrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x x_1 : { x // x ∈ H }), ↑(x - x_1) = ↑(x - x_1)

theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_6 {S : Type u_2} (H : S) {G : Type u_1} [LinearOrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x : { x // x ∈ H }), ↑(-x) = ↑(-x)

theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_10 {S : Type u_2} (H : S) {G : Type u_1} [LinearOrderedAddCommGroup G] [SetLike S G] : ∀ (x x_1 : { x // x ∈ H }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

theorem AddSubgroupClass.toLinearOrderedAddCommGroup.proof_8 {S : Type u_2} (H : S) {G : Type u_1} [LinearOrderedAddCommGroup G] [SetLike S G] [AddSubgroupClass S G] : ∀ (x : { x // x ∈ H }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

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

instance SubgroupClass.toLinearOrderedCommGroup {S : Type u_6} (H : S) {G : Type u_7} [LinearOrderedCommGroup G] [SetLike S G] [SubgroupClass S G] : LinearOrderedCommGroup { x // x ∈ H }

A subgroup of a LinearOrderedCommGroup is a LinearOrderedCommGroup.

def AddSubgroupClass.subtype {G : Type u_1} [AddGroup G] {S : Type u_6} (H : S) [SetLike S G] [AddSubgroupClass S G] : { x // x ∈ H } →+ G

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

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 : { x // x ∈ H }), ZeroHom.toFun { toFun := Subtype.val, map_zero' := (_ : ↑0 = ↑0) } (x + x_1) = ZeroHom.toFun { toFun := Subtype.val, map_zero' := (_ : ↑0 = ↑0) } (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 SubgroupClass.subtype {G : Type u_1} [Group G] {S : Type u_6} (H : S) [SetLike S G] [SubgroupClass S G] : { x // x ∈ H } →* G

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

@[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 : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // 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) : { x // x ∈ H } →+ { x // x ∈ K }

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

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 : { x // x ∈ H }), (fun x => { val := ↑x, property := h ↑x (_ : ↑x ∈ H) }) (x + x_1) = (fun x => { val := ↑x, property := h ↑x (_ : ↑x ∈ H) }) (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) : { x // x ∈ H } →* { x // x ∈ K }

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

@[simp]

theorem AddSubgroupClass.inclusion_self {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : { x // x ∈ H }) : ↑(AddSubgroupClass.inclusion (_ : H ≤ H)) 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 : { x // x ∈ H }) : ↑(SubgroupClass.inclusion (_ : H ≤ H)) 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) { val := x, property := hx } = { val := x, property := h x hx }

@[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) { val := x, property := hx } = { val := x, property := h x hx }

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 : { x // x ∈ K }) (hx : ↑x ∈ H) : ↑(AddSubgroupClass.inclusion h) { val := ↑x, property := 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 : { x // x ∈ K }) (hx : ↑x ∈ H) : ↑(SubgroupClass.inclusion h) { val := ↑x, property := 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 : { x // x ∈ H }) : ↑(SubgroupClass.inclusion hKL) (↑(SubgroupClass.inclusion hHK) x) = ↑(SubgroupClass.inclusion (_ : H ≤ L)) 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 : { x // x ∈ 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 : { x // x ∈ 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) : AddMonoidHom.comp (↑K) (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) : MonoidHom.comp (↑K) (SubgroupClass.inclusion hH) = ↑H

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

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

  G is closed under inverses

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

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

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

  G is closed under negation

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

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

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

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

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

theorem AddSubgroup.instAddSubgroupClassAddSubgroupToSubNegAddMonoidInstSetLikeAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] : AddSubgroupClass (AddSubgroup G) G

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

@[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 ∈ { toAddSubsemigroup := { carrier := s, add_mem' := h_one }, zero_mem' := h_mul }.toAddSubsemigroup.carrier → -x ∈ { toAddSubsemigroup := { carrier := s, add_mem' := h_one }, zero_mem' := h_mul }.toAddSubsemigroup.carrier) : x ∈ { toAddSubmonoid := { toAddSubsemigroup := { 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 ∈ { toSubsemigroup := { carrier := s, mul_mem' := h_one }, one_mem' := h_mul }.toSubsemigroup.carrier → x⁻¹ ∈ { toSubsemigroup := { carrier := s, mul_mem' := h_one }, one_mem' := h_mul }.toSubsemigroup.carrier) : x ∈ { toSubmonoid := { toSubsemigroup := { 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 ∈ { toAddSubsemigroup := { carrier := s, add_mem' := h_one }, zero_mem' := h_mul }.toAddSubsemigroup.carrier → -x ∈ { toAddSubsemigroup := { carrier := s, add_mem' := h_one }, zero_mem' := h_mul }.toAddSubsemigroup.carrier) : ↑{ toAddSubmonoid := { toAddSubsemigroup := { 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 ∈ { toSubsemigroup := { carrier := s, mul_mem' := h_one }, one_mem' := h_mul }.toSubsemigroup.carrier → x⁻¹ ∈ { toSubsemigroup := { carrier := s, mul_mem' := h_one }, one_mem' := h_mul }.toSubsemigroup.carrier) : ↑{ toSubmonoid := { toSubsemigroup := { 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 ∈ { toAddSubsemigroup := { carrier := s, add_mem' := h_one }, zero_mem' := h_mul }.toAddSubsemigroup.carrier → -x ∈ { toAddSubsemigroup := { carrier := s, add_mem' := h_one }, zero_mem' := h_mul }.toAddSubsemigroup.carrier) (h_one' : ∀ {a b : G}, a ∈ t → b ∈ t → a + b ∈ t) (h_mul' : t 0) (h_inv' : ∀ {x : G}, x ∈ { toAddSubsemigroup := { carrier := t, add_mem' := h_one' }, zero_mem' := h_mul' }.toAddSubsemigroup.carrier → -x ∈ { toAddSubsemigroup := { carrier := t, add_mem' := h_one' }, zero_mem' := h_mul' }.toAddSubsemigroup.carrier) : { toAddSubmonoid := { toAddSubsemigroup := { carrier := s, add_mem' := h_one }, zero_mem' := h_mul }, neg_mem' := h_inv } ≤ { toAddSubmonoid := { toAddSubsemigroup := { 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 ∈ { toSubsemigroup := { carrier := s, mul_mem' := h_one }, one_mem' := h_mul }.toSubsemigroup.carrier → x⁻¹ ∈ { toSubsemigroup := { carrier := s, mul_mem' := h_one }, one_mem' := h_mul }.toSubsemigroup.carrier) (h_one' : ∀ {a b : G}, a ∈ t → b ∈ t → a * b ∈ t) (h_mul' : t 1) (h_inv' : ∀ {x : G}, x ∈ { toSubsemigroup := { carrier := t, mul_mem' := h_one' }, one_mem' := h_mul' }.toSubsemigroup.carrier → x⁻¹ ∈ { toSubsemigroup := { carrier := t, mul_mem' := h_one' }, one_mem' := h_mul' }.toSubsemigroup.carrier) : { toSubmonoid := { toSubsemigroup := { carrier := s, mul_mem' := h_one }, one_mem' := h_mul }, inv_mem' := h_inv } ≤ { toSubmonoid := { toSubsemigroup := { 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

Conversion to/from Additive/Multiplicative

@[simp]

theorem Subgroup.toAddSubgroup_apply_coe {G : Type u_1} [Group G] (S : Subgroup G) : ↑(↑Subgroup.toAddSubgroup S) = ↑Additive.toMul ⁻¹' ↑S

@[simp]

theorem Subgroup.toAddSubgroup_symm_apply_coe {G : Type u_1} [Group G] (S : AddSubgroup (Additive G)) : ↑(↑(RelIso.symm Subgroup.toAddSubgroup) S) = ↑Multiplicative.toAdd ⁻¹' ↑S

def Subgroup.toAddSubgroup {G : Type u_1} [Group G] : Subgroup G ≃o AddSubgroup (Additive G)

Subgroups of a group G are isomorphic to additive subgroups of Additive G.

@[inline, reducible]

abbrev AddSubgroup.toSubgroup' {G : Type u_1} [Group G] : AddSubgroup (Additive G) ≃o Subgroup G

Additive subgroup of an additive group Additive G are isomorphic to subgroup of G.

@[simp]

theorem AddSubgroup.toSubgroup_apply_coe {A : Type u_4} [AddGroup A] (S : AddSubgroup A) : ↑(↑AddSubgroup.toSubgroup S) = ↑Multiplicative.toAdd ⁻¹' ↑S

@[simp]

theorem AddSubgroup.toSubgroup_symm_apply_coe {A : Type u_4} [AddGroup A] (S : Subgroup (Multiplicative A)) : ↑(↑(RelIso.symm AddSubgroup.toSubgroup) S) = ↑Additive.toMul ⁻¹' ↑S

def AddSubgroup.toSubgroup {A : Type u_4} [AddGroup A] : AddSubgroup A ≃o Subgroup (Multiplicative A)

Additive subgroups of an additive group A are isomorphic to subgroups of Multiplicative A.

@[inline, reducible]

abbrev Subgroup.toAddSubgroup' {A : Type u_4} [AddGroup A] : Subgroup (Multiplicative A) ≃o AddSubgroup A

Subgroups of an additive group Multiplicative A are isomorphic to additive subgroups of A.

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

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_2 {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = ↑K) : 0 ∈ { carrier := s, add_mem' := (_ : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier

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

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.

@[simp]

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

@[simp]

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

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

theorem Subgroup.copy_eq {G : Type u_1} [Group G] (K : Subgroup G) (s : Set G) (hs : s = ↑K) : Subgroup.copy K 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 {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.sub_mem_comm_iff {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {a : G} {b : G} : a - b ∈ H ↔ b - a ∈ H

theorem Subgroup.div_mem_comm_iff {G : Type u_1} [Group G] (H : Subgroup G) {a : G} {b : G} : a / b ∈ H ↔ b / a ∈ H

theorem AddSubgroup.exists_neg_mem_iff_exists_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {P : G → Prop} : (∃ x, x ∈ K ∧ P (-x)) ↔ ∃ 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, x ∈ K ∧ P x⁻¹) ↔ ∃ 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

def AddSubgroup.ofSub {G : Type u_1} [AddGroup G] (s : Set G) (hsn : Set.Nonempty s) (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

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

abbrev AddSubgroup.ofSub.match_1 {G : Type u_1} (s : Set G) (motive : Set.Nonempty s → Prop) : (hsn : Set.Nonempty s) → ((x : G) → (hx : x ∈ s) → motive (_ : ∃ x, x ∈ s)) → motive hsn

def Subgroup.ofDiv {G : Type u_1} [Group G] (s : Set G) (hsn : Set.Nonempty s) (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.

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

An AddSubgroup of an AddGroup inherits an addition.

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

A subgroup of a group inherits a multiplication.

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

An AddSubgroup of an AddGroup inherits a zero.

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

A subgroup of a group inherits a 1.

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

An AddSubgroup of an AddGroup inherits an inverse.

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

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

A subgroup of a group inherits an inverse.

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

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

An AddSubgroup of an AddGroup inherits a subtraction.

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

A subgroup of a group inherits a division

instance AddSubgroup.nsmul {G : Type u_5} [AddGroup G] {H : AddSubgroup G} : SMul ℕ { x // x ∈ H }

An AddSubgroup of an AddGroup inherits a natural scaling.

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

A subgroup of a group inherits a natural power

instance AddSubgroup.zsmul {G : Type u_5} [AddGroup G] {H : AddSubgroup G} : SMul ℤ { x // x ∈ H }

An AddSubgroup of an AddGroup inherits an integer scaling.

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

A subgroup of a group inherits an integer power

@[simp]

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

@[simp]

theorem Subgroup.coe_mul {G : Type u_1} [Group G] (H : Subgroup G) (x : { x // x ∈ H }) (y : { x // x ∈ 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 : { x // x ∈ H }) : ↑(-x) = -↑x

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem AddSubgroup.mk_eq_zero_iff {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {g : G} {h : g ∈ H} : { val := g, property := h } = 0 ↔ g = 0

@[simp]

theorem Subgroup.mk_eq_one_iff {G : Type u_1} [Group G] (H : Subgroup G) {g : G} {h : g ∈ H} : { val := g, property := h } = 1 ↔ g = 1

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

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

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

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

An AddSubgroup of an AddGroup inherits an AddGroup structure.

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

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

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

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

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

A subgroup of a group inherits a group structure.

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

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

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

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

An AddSubgroup of an AddCommGroup is an AddCommGroup.

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

theorem AddSubgroup.toAddCommGroup.proof_3 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) : ∀ (x x_1 : { x // x ∈ 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 => ↑a

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

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

A subgroup of a CommGroup is a CommGroup.

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

theorem AddSubgroup.toOrderedAddCommGroup.proof_7 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) : ∀ (x : { x // x ∈ H }) (x_1 : ℤ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubgroup.toOrderedAddCommGroup.proof_3 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) : ∀ (x x_1 : { x // x ∈ H }), ↑(x + x_1) = ↑(x + x_1)

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

theorem AddSubgroup.toOrderedAddCommGroup.proof_4 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) : ∀ (x : { x // x ∈ H }), ↑(-x) = ↑(-x)

instance AddSubgroup.toOrderedAddCommGroup {G : Type u_5} [OrderedAddCommGroup G] (H : AddSubgroup G) : OrderedAddCommGroup { x // x ∈ H }

An AddSubgroup of an AddOrderedCommGroup is an AddOrderedCommGroup.

theorem AddSubgroup.toOrderedAddCommGroup.proof_5 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) : ∀ (x x_1 : { x // x ∈ H }), ↑(x - x_1) = ↑(x - x_1)

theorem AddSubgroup.toOrderedAddCommGroup.proof_6 {G : Type u_1} [OrderedAddCommGroup G] (H : AddSubgroup G) : ∀ (x : { x // x ∈ H }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

instance Subgroup.toOrderedCommGroup {G : Type u_5} [OrderedCommGroup G] (H : Subgroup G) : OrderedCommGroup { x // x ∈ H }

A subgroup of an OrderedCommGroup is an OrderedCommGroup.

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_7 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) : ∀ (x : { x // x ∈ H }) (x_1 : ℤ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_9 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) : ∀ (x x_1 : { x // x ∈ H }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_5 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) : ∀ (x x_1 : { x // x ∈ H }), ↑(x - x_1) = ↑(x - x_1)

instance AddSubgroup.toLinearOrderedAddCommGroup {G : Type u_5} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) : LinearOrderedAddCommGroup { x // x ∈ H }

An AddSubgroup of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_8 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) : ∀ (x x_1 : { x // x ∈ H }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_6 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) : ∀ (x : { x // x ∈ H }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_4 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) : ∀ (x : { x // x ∈ H }), ↑(-x) = ↑(-x)

theorem AddSubgroup.toLinearOrderedAddCommGroup.proof_3 {G : Type u_1} [LinearOrderedAddCommGroup G] (H : AddSubgroup G) : ∀ (x x_1 : { x // x ∈ H }), ↑(x + x_1) = ↑(x + x_1)

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

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

instance Subgroup.toLinearOrderedCommGroup {G : Type u_5} [LinearOrderedCommGroup G] (H : Subgroup G) : LinearOrderedCommGroup { x // x ∈ H }

A subgroup of a LinearOrderedCommGroup is a LinearOrderedCommGroup.

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

theorem AddSubgroup.subtype.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ∀ (x x_1 : { x // x ∈ H }), ZeroHom.toFun { toFun := Subtype.val, map_zero' := (_ : ↑0 = ↑0) } (x + x_1) = ZeroHom.toFun { toFun := Subtype.val, map_zero' := (_ : ↑0 = ↑0) } (x + x_1)

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

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

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

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

@[simp]

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

@[simp]

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

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

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

theorem AddSubgroup.inclusion.proof_2 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) : ∀ (x x_1 : { x // x ∈ H }), (fun x => { val := ↑x, property := h ↑x (_ : ↑x ∈ H) }) (x + x_1) = (fun x => { val := ↑x, property := h ↑x (_ : ↑x ∈ H) }) (x + x_1)

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

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

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

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

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

@[simp]

theorem AddSubgroup.coe_inclusion {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {h : H ≤ K} (a : { x // x ∈ 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 : { x // x ∈ 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.subtype_comp_inclusion {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (hH : H ≤ K) : AddMonoidHom.comp (AddSubgroup.subtype K) (AddSubgroup.inclusion hH) = AddSubgroup.subtype H

@[simp]

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

theorem AddSubgroup.instTopAddSubgroup.proof_2 {G : Type u_1} [AddGroup G] : ∀ {x : G}, x ∈ { toAddSubsemigroup := ⊤.toAddSubsemigroup, zero_mem' := (_ : 0 ∈ ⊤.carrier) }.toAddSubsemigroup.carrier → -x ∈ Set.univ

theorem AddSubgroup.instTopAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] : 0 ∈ ⊤.carrier

instance AddSubgroup.instTopAddSubgroup {G : Type u_1} [AddGroup G] : Top (AddSubgroup G)

The AddSubgroup G of the AddGroup G.

instance Subgroup.instTopSubgroup {G : Type u_1} [Group G] : Top (Subgroup G)

The subgroup G of the group G.

def AddSubgroup.topEquiv {G : Type u_1} [AddGroup G] : { x // x ∈ ⊤ } ≃+ G

The top additive subgroup is isomorphic to the additive group.

This is the additive group version of AddSubmonoid.topEquiv.

@[simp]

theorem AddSubgroup.topEquiv_apply {G : Type u_1} [AddGroup G] (x : { x // x ∈ ⊤ }) : ↑AddSubgroup.topEquiv x = ↑x

@[simp]

theorem Subgroup.topEquiv_symm_apply_coe {G : Type u_1} [Group G] (x : G) : ↑(↑(MulEquiv.symm Subgroup.topEquiv) x) = x

@[simp]

theorem AddSubgroup.topEquiv_symm_apply_coe {G : Type u_1} [AddGroup G] (x : G) : ↑(↑(AddEquiv.symm AddSubgroup.topEquiv) x) = x

@[simp]

theorem Subgroup.topEquiv_apply {G : Type u_1} [Group G] (x : { x // x ∈ ⊤ }) : ↑Subgroup.topEquiv x = ↑x

def Subgroup.topEquiv {G : Type u_1} [Group G] : { x // x ∈ ⊤ } ≃* G

The top subgroup is isomorphic to the group.

This is the group version of Submonoid.topEquiv.

theorem AddSubgroup.instBotAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] : 0 ∈ ⊥.carrier

theorem AddSubgroup.instBotAddSubgroup.proof_2 {G : Type u_1} [AddGroup G] (a : G) : a ∈ ⊥.carrier → -a ∈ ⊥.carrier

instance AddSubgroup.instBotAddSubgroup {G : Type u_1} [AddGroup G] : Bot (AddSubgroup G)

The trivial AddSubgroup {0} of an AddGroup G.

instance Subgroup.instBotSubgroup {G : Type u_1} [Group G] : Bot (Subgroup G)

The trivial subgroup {1} of a group G.

instance AddSubgroup.instInhabitedAddSubgroup {G : Type u_1} [AddGroup G] : Inhabited (AddSubgroup G)

instance Subgroup.instInhabitedSubgroup {G : Type u_1} [Group G] : Inhabited (Subgroup G)

@[simp]

theorem AddSubgroup.mem_bot {G : Type u_1} [AddGroup G] {x : G} : x ∈ ⊥ ↔ x = 0

@[simp]

theorem Subgroup.mem_bot {G : Type u_1} [Group G] {x : G} : x ∈ ⊥ ↔ x = 1

@[simp]

theorem AddSubgroup.mem_top {G : Type u_1} [AddGroup G] (x : G) : x ∈ ⊤

@[simp]

theorem Subgroup.mem_top {G : Type u_1} [Group G] (x : G) : x ∈ ⊤

@[simp]

theorem AddSubgroup.coe_top {G : Type u_1} [AddGroup G] : ↑⊤ = Set.univ

@[simp]

theorem Subgroup.coe_top {G : Type u_1} [Group G] : ↑⊤ = Set.univ

@[simp]

theorem AddSubgroup.coe_bot {G : Type u_1} [AddGroup G] : ↑⊥ = {0}

@[simp]

theorem Subgroup.coe_bot {G : Type u_1} [Group G] : ↑⊥ = {1}

theorem AddSubgroup.instUniqueSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupBotInstBotAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] (g : { x // x ∈ ⊥ }) : g = default

instance AddSubgroup.instUniqueSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupBotInstBotAddSubgroup {G : Type u_1} [AddGroup G] : Unique { x // x ∈ ⊥ }

instance Subgroup.instUniqueSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupBotInstBotSubgroup {G : Type u_1} [Group G] : Unique { x // x ∈ ⊥ }

@[simp]

theorem AddSubgroup.top_toAddSubmonoid {G : Type u_1} [AddGroup G] : ⊤.toAddSubmonoid = ⊤

@[simp]

theorem Subgroup.top_toSubmonoid {G : Type u_1} [Group G] : ⊤.toSubmonoid = ⊤

@[simp]

theorem AddSubgroup.bot_toAddSubmonoid {G : Type u_1} [AddGroup G] : ⊥.toAddSubmonoid = ⊥

@[simp]

theorem Subgroup.bot_toSubmonoid {G : Type u_1} [Group G] : ⊥.toSubmonoid = ⊥

theorem AddSubgroup.eq_bot_iff_forall {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H = ⊥ ↔ ∀ (x : G), x ∈ H → x = 0

theorem Subgroup.eq_bot_iff_forall {G : Type u_1} [Group G] (H : Subgroup G) : H = ⊥ ↔ ∀ (x : G), x ∈ H → x = 1

theorem AddSubgroup.eq_bot_of_subsingleton {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Subsingleton { x // x ∈ H }] : H = ⊥

theorem Subgroup.eq_bot_of_subsingleton {G : Type u_1} [Group G] (H : Subgroup G) [Subsingleton { x // x ∈ H }] : H = ⊥

theorem AddSubgroup.coe_eq_univ {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : ↑H = Set.univ ↔ H = ⊤

theorem Subgroup.coe_eq_univ {G : Type u_1} [Group G] {H : Subgroup G} : ↑H = Set.univ ↔ H = ⊤

theorem AddSubgroup.coe_eq_singleton {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : (∃ g, ↑H = {g}) ↔ H = ⊥

abbrev AddSubgroup.coe_eq_singleton.match_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (motive : (∃ g, ↑H = {g}) → Prop) : (x : ∃ g, ↑H = {g}) → ((g : G) → (hg : ↑H = {g}) → motive (_ : ∃ g, ↑H = {g})) → motive x

theorem Subgroup.coe_eq_singleton {G : Type u_1} [Group G] {H : Subgroup G} : (∃ g, ↑H = {g}) ↔ H = ⊥

theorem AddSubgroup.nontrivial_iff_exists_ne_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Nontrivial { x // x ∈ H } ↔ ∃ x, x ∈ H ∧ x ≠ 0

theorem Subgroup.nontrivial_iff_exists_ne_one {G : Type u_1} [Group G] (H : Subgroup G) : Nontrivial { x // x ∈ H } ↔ ∃ x, x ∈ H ∧ x ≠ 1

theorem AddSubgroup.exists_ne_zero_of_nontrivial {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Nontrivial { x // x ∈ H }] : ∃ x, x ∈ H ∧ x ≠ 0

theorem Subgroup.exists_ne_one_of_nontrivial {G : Type u_1} [Group G] (H : Subgroup G) [Nontrivial { x // x ∈ H }] : ∃ x, x ∈ H ∧ x ≠ 1

theorem AddSubgroup.nontrivial_iff_ne_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Nontrivial { x // x ∈ H } ↔ H ≠ ⊥

theorem Subgroup.nontrivial_iff_ne_bot {G : Type u_1} [Group G] (H : Subgroup G) : Nontrivial { x // x ∈ H } ↔ H ≠ ⊥

theorem AddSubgroup.bot_or_nontrivial {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H = ⊥ ∨ Nontrivial { x // x ∈ H }

A subgroup is either the trivial subgroup or nontrivial.

theorem Subgroup.bot_or_nontrivial {G : Type u_1} [Group G] (H : Subgroup G) : H = ⊥ ∨ Nontrivial { x // x ∈ H }

A subgroup is either the trivial subgroup or nontrivial.

theorem AddSubgroup.bot_or_exists_ne_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H = ⊥ ∨ ∃ x, x ∈ H ∧ x ≠ 0

A subgroup is either the trivial subgroup or contains a nonzero element.

theorem Subgroup.bot_or_exists_ne_one {G : Type u_1} [Group G] (H : Subgroup G) : H = ⊥ ∨ ∃ x, x ∈ H ∧ x ≠ 1

A subgroup is either the trivial subgroup or contains a non-identity element.

theorem AddSubgroup.ne_bot_iff_exists_ne_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H ≠ ⊥ ↔ ∃ a, a ≠ 0

theorem Subgroup.ne_bot_iff_exists_ne_one {G : Type u_1} [Group G] {H : Subgroup G} : H ≠ ⊥ ↔ ∃ a, a ≠ 1

instance AddSubgroup.instInfAddSubgroup {G : Type u_1} [AddGroup G] : Inf (AddSubgroup G)

The inf of two AddSubgroups is their intersection.

theorem AddSubgroup.instInfAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] (H₁ : AddSubgroup G) (H₂ : AddSubgroup G) : 0 ∈ (H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid).carrier

abbrev AddSubgroup.instInfAddSubgroup.match_1 {G : Type u_1} [AddGroup G] (H₁ : AddSubgroup G) (H₂ : AddSubgroup G) : {x : G} → let src := H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid; ∀ (motive : x ∈ { toAddSubsemigroup := src.toAddSubsemigroup, zero_mem' := (_ : 0 ∈ src.carrier) }.toAddSubsemigroup.carrier → Prop) (x_1 : x ∈ { toAddSubsemigroup := src.toAddSubsemigroup, zero_mem' := (_ : 0 ∈ src.carrier) }.toAddSubsemigroup.carrier), (∀ (hx : x ∈ ↑H₁.toAddSubmonoid) (hx' : x ∈ ↑H₂.toAddSubmonoid), motive (_ : x ∈ ↑H₁.toAddSubmonoid ∧ x ∈ ↑H₂.toAddSubmonoid)) → motive x_1

theorem AddSubgroup.instInfAddSubgroup.proof_2 {G : Type u_1} [AddGroup G] (H₁ : AddSubgroup G) (H₂ : AddSubgroup G) : ∀ {x : G}, x ∈ { toAddSubsemigroup := (H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid).toAddSubsemigroup, zero_mem' := (_ : 0 ∈ (H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid).carrier) }.toAddSubsemigroup.carrier → -x ∈ { toAddSubsemigroup := (H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid).toAddSubsemigroup, zero_mem' := (_ : 0 ∈ (H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid).carrier) }.toAddSubsemigroup.carrier

instance Subgroup.instInfSubgroup {G : Type u_1} [Group G] : Inf (Subgroup G)

The inf of two subgroups is their intersection.

@[simp]

theorem AddSubgroup.coe_inf {G : Type u_1} [AddGroup G] (p : AddSubgroup G) (p' : AddSubgroup G) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem Subgroup.coe_inf {G : Type u_1} [Group G] (p : Subgroup G) (p' : Subgroup G) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem AddSubgroup.mem_inf {G : Type u_1} [AddGroup G] {p : AddSubgroup G} {p' : AddSubgroup G} {x : G} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

@[simp]

theorem Subgroup.mem_inf {G : Type u_1} [Group G] {p : Subgroup G} {p' : Subgroup G} {x : G} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

theorem AddSubgroup.instInfSetAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) : ⋂ (S : AddSubgroup G) (_ : S ∈ s), ↑S = ↑(⨅ (i : AddSubgroup G) (_ : i ∈ s), i.toAddSubmonoid)

instance AddSubgroup.instInfSetAddSubgroup {G : Type u_1} [AddGroup G] : InfSet (AddSubgroup G)

theorem AddSubgroup.instInfSetAddSubgroup.proof_2 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) : 0 ∈ (AddSubmonoid.copy (⨅ (S : AddSubgroup G) (_ : S ∈ s), S.toAddSubmonoid) (⋂ (S : AddSubgroup G) (_ : S ∈ s), ↑S) (_ : ⋂ (S : AddSubgroup G) (_ : S ∈ s), ↑S = ↑(⨅ (i : AddSubgroup G) (_ : i ∈ s), i.toAddSubmonoid))).toAddSubsemigroup.carrier

theorem AddSubgroup.instInfSetAddSubgroup.proof_3 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) {x : G} (hx : x ∈ { toAddSubsemigroup := (AddSubmonoid.copy (⨅ (S : AddSubgroup G) (_ : S ∈ s), S.toAddSubmonoid) (⋂ (S : AddSubgroup G) (_ : S ∈ s), ↑S) (_ : ⋂ (S : AddSubgroup G) (_ : S ∈ s), ↑S = ↑(⨅ (i : AddSubgroup G) (_ : i ∈ s), i.toAddSubmonoid))).toAddSubsemigroup, zero_mem' := (_ : 0 ∈ (AddSubmonoid.copy (⨅ (S : AddSubgroup G) (_ : S ∈ s), S.toAddSubmonoid) (⋂ (S : AddSubgroup G) (_ : S ∈ s), ↑S) (_ : ⋂ (S : AddSubgroup G) (_ : S ∈ s), ↑S = ↑(⨅ (i : AddSubgroup G) (_ : i ∈ s), i.toAddSubmonoid))).toAddSubsemigroup.carrier) }.toAddSubsemigroup.carrier) : -x ∈ ⋂ (x : AddSubgroup G) (_ : x ∈ s), ↑x

instance Subgroup.instInfSetSubgroup {G : Type u_1} [Group G] : InfSet (Subgroup G)

@[simp]

theorem AddSubgroup.coe_sInf {G : Type u_1} [AddGroup G] (H : Set (AddSubgroup G)) : ↑(sInf H) = ⋂ (s : AddSubgroup G) (_ : s ∈ H), ↑s

@[simp]

theorem Subgroup.coe_sInf {G : Type u_1} [Group G] (H : Set (Subgroup G)) : ↑(sInf H) = ⋂ (s : Subgroup G) (_ : s ∈ H), ↑s

@[simp]

theorem AddSubgroup.mem_sInf {G : Type u_1} [AddGroup G] {S : Set (AddSubgroup G)} {x : G} : x ∈ sInf S ↔ ∀ (p : AddSubgroup G), p ∈ S → x ∈ p

@[simp]

theorem Subgroup.mem_sInf {G : Type u_1} [Group G] {S : Set (Subgroup G)} {x : G} : x ∈ sInf S ↔ ∀ (p : Subgroup G), p ∈ S → x ∈ p

theorem AddSubgroup.mem_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_5} {S : ι → AddSubgroup G} {x : G} : x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

theorem Subgroup.mem_iInf {G : Type u_1} [Group G] {ι : Sort u_5} {S : ι → Subgroup G} {x : G} : x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

@[simp]

theorem AddSubgroup.coe_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_5} {S : ι → AddSubgroup G} : ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

@[simp]

theorem Subgroup.coe_iInf {G : Type u_1} [Group G] {ι : Sort u_5} {S : ι → Subgroup G} : ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

instance AddSubgroup.instCompleteLatticeAddSubgroup {G : Type u_1} [AddGroup G] : CompleteLattice (AddSubgroup G)

The AddSubgroups of an AddGroup form a complete lattice.

theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] (_s : Set (AddSubgroup G)) : IsGLB _s (sInf _s)

theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_8 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) : (∀ (b : AddSubgroup G), b ∈ s → a ≤ b) → a ≤ sInf s

theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_9 {G : Type u_1} [AddGroup G] (S : AddSubgroup G) (_x : G) (hx : _x ∈ ⊥) : _x ∈ S

theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_3 {G : Type u_1} [AddGroup G] (_a : AddSubgroup G) (_b : AddSubgroup G) (_x : G) (self : _x ∈ ↑_a.toAddSubmonoid ∧ _x ∈ ↑_b.toAddSubmonoid) : _x ∈ ↑_b.toAddSubmonoid

theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_7 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) : a ∈ s → sInf s ≤ a

theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_5 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) : a ∈ s → a ≤ sSup s

theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_6 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) : (∀ (b : AddSubgroup G), b ∈ s → b ≤ a) → sSup s ≤ a

theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_4 {G : Type u_1} [AddGroup G] (_a : AddSubgroup G) (_b : AddSubgroup G) (_c : AddSubgroup G) (ha : _a ≤ _b) (hb : _a ≤ _c) (_x : G) (hx : _x ∈ _a) : _x ∈ ↑_b.toAddSubmonoid ∧ _x ∈ ↑_c.toAddSubmonoid

theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_2 {G : Type u_1} [AddGroup G] (_a : AddSubgroup G) (_b : AddSubgroup G) (_x : G) (self : _x ∈ ↑_a.toAddSubmonoid ∧ _x ∈ ↑_b.toAddSubmonoid) : _x ∈ ↑_a.toAddSubmonoid

instance Subgroup.instCompleteLatticeSubgroup {G : Type u_1} [Group G] : CompleteLattice (Subgroup G)

Subgroups of a group form a complete lattice.

theorem AddSubgroup.mem_sup_left {G : Type u_1} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} {x : G} : x ∈ S → x ∈ S ⊔ T

theorem Subgroup.mem_sup_left {G : Type u_1} [Group G] {S : Subgroup G} {T : Subgroup G} {x : G} : x ∈ S → x ∈ S ⊔ T

theorem AddSubgroup.mem_sup_right {G : Type u_1} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} {x : G} : x ∈ T → x ∈ S ⊔ T

theorem Subgroup.mem_sup_right {G : Type u_1} [Group G] {S : Subgroup G} {T : Subgroup G} {x : G} : x ∈ T → x ∈ S ⊔ T

theorem AddSubgroup.add_mem_sup {G : Type u_1} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} {x : G} {y : G} (hx : x ∈ S) (hy : y ∈ T) : x + y ∈ S ⊔ T

theorem Subgroup.mul_mem_sup {G : Type u_1} [Group G] {S : Subgroup G} {T : Subgroup G} {x : G} {y : G} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T

theorem AddSubgroup.mem_iSup_of_mem {G : Type u_1} [AddGroup G] {ι : Sort u_5} {S : ι → AddSubgroup G} (i : ι) {x : G} : x ∈ S i → x ∈ iSup S

theorem Subgroup.mem_iSup_of_mem {G : Type u_1} [Group G] {ι : Sort u_5} {S : ι → Subgroup G} (i : ι) {x : G} : x ∈ S i → x ∈ iSup S

theorem AddSubgroup.mem_sSup_of_mem {G : Type u_1} [AddGroup G] {S : Set (AddSubgroup G)} {s : AddSubgroup G} (hs : s ∈ S) {x : G} : x ∈ s → x ∈ sSup S

theorem Subgroup.mem_sSup_of_mem {G : Type u_1} [Group G] {S : Set (Subgroup G)} {s : Subgroup G} (hs : s ∈ S) {x : G} : x ∈ s → x ∈ sSup S

@[simp]

theorem AddSubgroup.subsingleton_iff {G : Type u_1} [AddGroup G] : Subsingleton (AddSubgroup G) ↔ Subsingleton G

@[simp]

theorem Subgroup.subsingleton_iff {G : Type u_1} [Group G] : Subsingleton (Subgroup G) ↔ Subsingleton G

@[simp]

theorem AddSubgroup.nontrivial_iff {G : Type u_1} [AddGroup G] : Nontrivial (AddSubgroup G) ↔ Nontrivial G

@[simp]

theorem Subgroup.nontrivial_iff {G : Type u_1} [Group G] : Nontrivial (Subgroup G) ↔ Nontrivial G

theorem AddSubgroup.instUniqueAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] [Subsingleton G] (a : AddSubgroup G) : a = default

instance AddSubgroup.instUniqueAddSubgroup {G : Type u_1} [AddGroup G] [Subsingleton G] : Unique (AddSubgroup G)

instance Subgroup.instUniqueSubgroup {G : Type u_1} [Group G] [Subsingleton G] : Unique (Subgroup G)

theorem AddSubgroup.instNontrivialAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] [Nontrivial G] : Nontrivial (AddSubgroup G)

instance AddSubgroup.instNontrivialAddSubgroup {G : Type u_1} [AddGroup G] [Nontrivial G] : Nontrivial (AddSubgroup G)

instance Subgroup.instNontrivialSubgroup {G : Type u_1} [Group G] [Nontrivial G] : Nontrivial (Subgroup G)

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

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

def AddSubgroup.closure {G : Type u_1} [AddGroup G] (k : Set G) : AddSubgroup G

The AddSubgroup generated by a set

def Subgroup.closure {G : Type u_1} [Group G] (k : Set G) : Subgroup G

The Subgroup generated by a set.

theorem AddSubgroup.mem_closure {G : Type u_1} [AddGroup G] {k : Set G} {x : G} : x ∈ AddSubgroup.closure k ↔ ∀ (K : AddSubgroup G), k ⊆ ↑K → x ∈ K

theorem Subgroup.mem_closure {G : Type u_1} [Group G] {k : Set G} {x : G} : x ∈ Subgroup.closure k ↔ ∀ (K : Subgroup G), k ⊆ ↑K → x ∈ K

@[simp]

theorem AddSubgroup.subset_closure {G : Type u_1} [AddGroup G] {k : Set G} : k ⊆ ↑(AddSubgroup.closure k)

The AddSubgroup generated by a set includes the set.

@[simp]

theorem Subgroup.subset_closure {G : Type u_1} [Group G] {k : Set G} : k ⊆ ↑(Subgroup.closure k)

The subgroup generated by a set includes the set.

theorem AddSubgroup.not_mem_of_not_mem_closure {G : Type u_1} [AddGroup G] {k : Set G} {P : G} (hP : ¬P ∈ AddSubgroup.closure k) : ¬P ∈ k

theorem Subgroup.not_mem_of_not_mem_closure {G : Type u_1} [Group G] {k : Set G} {P : G} (hP : ¬P ∈ Subgroup.closure k) : ¬P ∈ k

@[simp]

theorem AddSubgroup.closure_le {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {k : Set G} : AddSubgroup.closure k ≤ K ↔ k ⊆ ↑K

An additive subgroup K includes closure k if and only if it includes k

@[simp]

theorem Subgroup.closure_le {G : Type u_1} [Group G] (K : Subgroup G) {k : Set G} : Subgroup.closure k ≤ K ↔ k ⊆ ↑K

A subgroup K includes closure k if and only if it includes k.

theorem AddSubgroup.closure_eq_of_le {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {k : Set G} (h₁ : k ⊆ ↑K) (h₂ : K ≤ AddSubgroup.closure k) : AddSubgroup.closure k = K

theorem Subgroup.closure_eq_of_le {G : Type u_1} [Group G] (K : Subgroup G) {k : Set G} (h₁ : k ⊆ ↑K) (h₂ : K ≤ Subgroup.closure k) : Subgroup.closure k = K

theorem AddSubgroup.closure_induction {G : Type u_1} [AddGroup G] {k : Set G} {p : G → Prop} {x : G} (h : x ∈ AddSubgroup.closure k) (Hk : (x : G) → x ∈ k → p x) (H1 : p 0) (Hmul : (x y : G) → p x → p y → p (x + y)) (Hinv : (x : G) → p x → p (-x)) : p x

An induction principle for additive closure membership. If p holds for 0 and all elements of k, and is preserved under addition and inverses, then p holds for all elements of the additive closure of k.

theorem Subgroup.closure_induction {G : Type u_1} [Group G] {k : Set G} {p : G → Prop} {x : G} (h : x ∈ Subgroup.closure k) (Hk : (x : G) → x ∈ k → p x) (H1 : p 1) (Hmul : (x y : G) → p x → p y → p (x * y)) (Hinv : (x : G) → p x → p x⁻¹) : p x

An induction principle for closure membership. If p holds for 1 and all elements of k, and is preserved under multiplication and inverse, then p holds for all elements of the closure of k.

theorem AddSubgroup.closure_induction' {G : Type u_1} [AddGroup G] {k : Set G} {p : (x : G) → x ∈ AddSubgroup.closure k → Prop} (Hs : (x : G) → (h : x ∈ k) → p x (_ : x ∈ ↑(AddSubgroup.closure k))) (H1 : p 0 (_ : 0 ∈ AddSubgroup.closure k)) (Hmul : (x : G) → (hx : x ∈ AddSubgroup.closure k) → (y : G) → (hy : y ∈ AddSubgroup.closure k) → p x hx → p y hy → p (x + y) (_ : x + y ∈ AddSubgroup.closure k)) (Hinv : (x : G) → (hx : x ∈ AddSubgroup.closure k) → p x hx → p (-x) (_ : -x ∈ AddSubgroup.closure k)) {x : G} (hx : x ∈ AddSubgroup.closure k) : p x hx

A dependent version of AddSubgroup.closure_induction.

abbrev AddSubgroup.closure_induction'.match_1 {G : Type u_1} [AddGroup G] {k : Set G} {p : (x : G) → x ∈ AddSubgroup.closure k → Prop} (y : G) (motive : (∃ x, p y x) → Prop) : (x : ∃ x, p y x) → ((hy' : y ∈ AddSubgroup.closure k) → (hy : p y hy') → motive (_ : ∃ x, p y x)) → motive x

theorem Subgroup.closure_induction' {G : Type u_1} [Group G] {k : Set G} {p : (x : G) → x ∈ Subgroup.closure k → Prop} (Hs : (x : G) → (h : x ∈ k) → p x (_ : x ∈ ↑(Subgroup.closure k))) (H1 : p 1 (_ : 1 ∈ Subgroup.closure k)) (Hmul : (x : G) → (hx : x ∈ Subgroup.closure k) → (y : G) → (hy : y ∈ Subgroup.closure k) → p x hx → p y hy → p (x * y) (_ : x * y ∈ Subgroup.closure k)) (Hinv : (x : G) → (hx : x ∈ Subgroup.closure k) → p x hx → p x⁻¹ (_ : x⁻¹ ∈ Subgroup.closure k)) {x : G} (hx : x ∈ Subgroup.closure k) : p x hx

A dependent version of Subgroup.closure_induction.

theorem AddSubgroup.closure_induction₂ {G : Type u_1} [AddGroup G] {k : Set G} {p : G → G → Prop} {x : G} {y : G} (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k) (Hk : (x : G) → x ∈ k → (y : G) → y ∈ k → p x y) (H1_left : (x : G) → p 0 x) (H1_right : (x : G) → p x 0) (Hmul_left : (x₁ x₂ y : G) → p x₁ y → p x₂ y → p (x₁ + x₂) y) (Hmul_right : (x y₁ y₂ : G) → p x y₁ → p x y₂ → p x (y₁ + y₂)) (Hinv_left : (x y : G) → p x y → p (-x) y) (Hinv_right : (x y : G) → p x y → p x (-y)) : p x y

An induction principle for additive closure membership, for predicates with two arguments.

theorem Subgroup.closure_induction₂ {G : Type u_1} [Group G] {k : Set G} {p : G → G → Prop} {x : G} {y : G} (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k) (Hk : (x : G) → x ∈ k → (y : G) → y ∈ k → p x y) (H1_left : (x : G) → p 1 x) (H1_right : (x : G) → p x 1) (Hmul_left : (x₁ x₂ y : G) → p x₁ y → p x₂ y → p (x₁ * x₂) y) (Hmul_right : (x y₁ y₂ : G) → p x y₁ → p x y₂ → p x (y₁ * y₂)) (Hinv_left : (x y : G) → p x y → p x⁻¹ y) (Hinv_right : (x y : G) → p x y → p x y⁻¹) : p x y

An induction principle for closure membership for predicates with two arguments.

@[simp]

theorem AddSubgroup.closure_closure_coe_preimage {G : Type u_1} [AddGroup G] {k : Set G} : AddSubgroup.closure (Subtype.val ⁻¹' k) = ⊤

@[simp]

theorem Subgroup.closure_closure_coe_preimage {G : Type u_1} [Group G] {k : Set G} : Subgroup.closure (Subtype.val ⁻¹' k) = ⊤

def AddSubgroup.closureAddCommGroupOfComm {G : Type u_1} [AddGroup G] {k : Set G} (hcomm : ∀ (x : G), x ∈ k → ∀ (y : G), y ∈ k → x + y = y + x) : AddCommGroup { x // x ∈ AddSubgroup.closure k }

If all the elements of a set s commute, then closure s is an additive commutative group.

theorem AddSubgroup.closureAddCommGroupOfComm.proof_1 {G : Type u_1} [AddGroup G] {k : Set G} (a : { x // x ∈ AddSubgroup.closure k }) : -a + a = 0

theorem AddSubgroup.closureAddCommGroupOfComm.proof_2 {G : Type u_1} [AddGroup G] {k : Set G} (hcomm : ∀ (x : G), x ∈ k → ∀ (y : G), y ∈ k → x + y = y + x) (x : { x // x ∈ AddSubgroup.closure k }) (y : { x // x ∈ AddSubgroup.closure k }) : x + y = y + x

def Subgroup.closureCommGroupOfComm {G : Type u_1} [Group G] {k : Set G} (hcomm : ∀ (x : G), x ∈ k → ∀ (y : G), y ∈ k → x * y = y * x) : CommGroup { x // x ∈ Subgroup.closure k }

If all the elements of a set s commute, then closure s is a commutative group.

def AddSubgroup.gi (G : Type u_1) [AddGroup G] : GaloisInsertion AddSubgroup.closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

theorem AddSubgroup.gi.proof_1 (G : Type u_1) [AddGroup G] (_s : AddSubgroup G) : ↑_s ⊆ ↑(AddSubgroup.closure ↑_s)

theorem AddSubgroup.gi.proof_2 (G : Type u_1) [AddGroup G] (_s : Set G) (_h : ↑(AddSubgroup.closure _s) ≤ _s) : (fun s x => AddSubgroup.closure s) _s _h = (fun s x => AddSubgroup.closure s) _s _h

def Subgroup.gi (G : Type u_1) [Group G] : GaloisInsertion Subgroup.closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

theorem AddSubgroup.closure_mono {G : Type u_1} [AddGroup G] ⦃h : Set G⦄ ⦃k : Set G⦄ (h' : h ⊆ k) : AddSubgroup.closure h ≤ AddSubgroup.closure k

Additive subgroup closure of a set is monotone in its argument: if h ⊆ k, then closure h ≤ closure k

theorem Subgroup.closure_mono {G : Type u_1} [Group G] ⦃h : Set G⦄ ⦃k : Set G⦄ (h' : h ⊆ k) : Subgroup.closure h ≤ Subgroup.closure k

Subgroup closure of a set is monotone in its argument: if h ⊆ k, then closure h ≤ closure k.

@[simp]

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

Additive closure of an additive subgroup K equals K

@[simp]</