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→* 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× K is a subgroup of G × N× 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

ink

class InvMemClass (S : Type u_1) (G : Type u_2) [inst : Inv G] [inst : SetLike S G] : Prop

• s is closed under inverses

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

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

ink

class NegMemClass (S : Type u_1) (G : Type u_2) [inst : Neg G] [inst : SetLike S G] : Prop

• s is closed under negation

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

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

ink

class SubgroupClass (S : Type u_1) (G : Type u_2) [inst : DivInvMonoid G] [inst : SetLike S G] extends SubmonoidClass , InvMemClass : Prop

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

ink

class AddSubgroupClass (S : Type u_1) (G : Type u_2) [inst : SubNegMonoid G] [inst : SetLike S G] extends AddSubmonoidClass , NegMemClass : Prop

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem abs_mem_iff {S : Type u_1} {G : Type u_2} [inst : InvolutiveNeg G] [inst : LinearOrder G] : ∀ {x : SetLike S G} [inst : NegMemClass S G] {H : S} {x_1 : G}, abs x_1 ∈ H ↔ x_1 ∈ H

ink

theorem sub_mem {M : Type u_1} {S : Type u_2} [inst : SubNegMonoid M] [inst : 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.

ink

theorem div_mem {M : Type u_1} {S : Type u_2} [inst : DivInvMonoid M] [inst : 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.

ink

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

ink

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

Equations

• zsmul_mem.match_1 motive x h_1 h_2 = Int.casesOn x (fun a => h_1 a) fun a => h_2 a

ink

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

ink

theorem sub_mem_comm_iff {G : Type u_1} [inst : AddGroup G] {S : Type u_2} {H : S} [inst : SetLike S G] [inst : AddSubgroupClass S G] {a : G} {b : G} : a - b ∈ H ↔ b - a ∈ H

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

An additive subgroup of a add_group inherits an inverse.

Equations

• AddSubgroupClass.neg = { neg := fun a => { val := -↑a, property := (_ : -↑a ∈ H) } }

ink

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

Equations

• (_ : -↑a ∈ H) = (_ : -↑a ∈ H)

ink

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

A subgroup of a group inherits an inverse.

Equations

• SubgroupClass.inv = { inv := fun a => { val := (↑a)⁻¹, property := (_ : (↑a)⁻¹ ∈ H) } }

ink

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

Equations

• (_ : ↑a - ↑b ∈ H) = (_ : ↑a - ↑b ∈ H)

ink

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

An additive subgroup of an add_group inherits a subtraction.

Equations

• AddSubgroupClass.sub = { sub := fun a b => { val := ↑a - ↑b, property := (_ : ↑a - ↑b ∈ H) } }

ink

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

A subgroup of a group inherits a division

Equations

• SubgroupClass.div = { div := fun a b => { val := ↑a / ↑b, property := (_ : ↑a / ↑b ∈ H) } }

ink

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

An additive subgroup of an add_group inherits an integer scaling.

Equations

• AddSubgroupClass.zsmul = { smul := fun n a => { val := n • ↑a, property := (_ : n • ↑a ∈ H) } }

ink

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

A subgroup of a group inherits an integer power.

Equations

• SubgroupClass.zpow = { pow := fun a n => { val := ↑a ^ n, property := (_ : ↑a ^ n ∈ H) } }

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem AddSubgroupClass.coe_sub {G : Type u_1} [inst : AddGroup G] {S : Type u_2} {H : S} [inst : SetLike S G] [inst : AddSubgroupClass S G] (x : { x // x ∈ H }) (y : { x // x ∈ H }) : ↑(x - y) = ↑x - ↑y

ink

@[simp]

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

ink

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

Equations

• (_ : ZeroMemClass S G) = (_ : ZeroMemClass S G)

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

ink

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

Equations

• (_ : AddSubmonoidClass S G) = (_ : AddSubmonoidClass S G)

ink

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

Equations

• (_ : ↑(x - x) = ↑(x - x)) = (_ : ↑(x - x) = ↑(x - x))

ink

def AddSubgroupClass.toAddGroup.proof_8 {G : Type u_1} [inst : AddGroup G] {S : Type u_2} (H : S) [inst : SetLike S G] [inst : AddSubgroupClass S G] : ∀ (x : { x // x ∈ H }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

ink

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

Equations

• (_ : ↑(-x) = ↑(-x)) = (_ : ↑(-x) = ↑(-x))

ink

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

An additive subgroup of an AddGroup inherits an AddGroup structure.

Equations

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

ink

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

Equations

• (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

ink

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

A subgroup of a group inherits a group structure.

Equations

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

ink

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

An additive subgroup of an AddCommGroup is an AddCommGroup.

Equations

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

ink

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

Equations

• (_ : AddSubmonoidClass S G) = (_ : AddSubmonoidClass S G)

ink

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

Equations

• (_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

ink

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

Equations

• (_ : ZeroMemClass S G) = (_ : ZeroMemClass S G)

ink

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

Equations

• (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

ink

def AddSubgroupClass.toAddCommGroup.proof_8 {S : Type u_2} (H : S) {G : Type u_1} [inst : AddCommGroup G] [inst : SetLike S G] [inst : AddSubgroupClass S G] : ∀ (x : { x // x ∈ H }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ↑(-x) = ↑(-x)) = (_ : ↑(-x) = ↑(-x))

ink

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

Equations

• (_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

ink

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

Equations

• (_ : ↑(x - x) = ↑(x - x)) = (_ : ↑(x - x) = ↑(x - x))

ink

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

A subgroup of a CommGroup is a CommGroup.

Equations

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

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

ink

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

Equations

• (_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

ink

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

Equations

• (_ : AddSubmonoidClass S G) = (_ : AddSubmonoidClass S G)

ink

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

An additive subgroup of an AddOrderedCommGroup is an AddOrderedCommGroup.

Equations

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

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ↑(x - x) = ↑(x - x)) = (_ : ↑(x - x) = ↑(x - x))

ink

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

Equations

• (_ : ↑(-x) = ↑(-x)) = (_ : ↑(-x) = ↑(-x))

ink

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

Equations

• (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

ink

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

Equations

• (_ : ZeroMemClass S G) = (_ : ZeroMemClass S G)

ink

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

A subgroup of an OrderedCommGroup is an OrderedCommGroup.

Equations

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

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ↑(x ⊓ x) = ↑(x ⊓ x)) = (_ : ↑(x ⊓ x) = ↑(x ⊓ x))

ink

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

Equations

• (_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

ink

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

Equations

• (_ : ↑(x ⊔ x) = ↑(x ⊔ x)) = (_ : ↑(x ⊔ x) = ↑(x ⊔ x))

ink

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

Equations

• (_ : ↑(-x) = ↑(-x)) = (_ : ↑(-x) = ↑(-x))

ink

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

Equations

• (_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

ink

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

Equations

• (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

ink

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

An additive subgroup of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

Equations

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

ink

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

Equations

• (_ : AddSubmonoidClass S G) = (_ : AddSubmonoidClass S G)

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ZeroMemClass S G) = (_ : ZeroMemClass S G)

ink

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

Equations

• (_ : ↑(x - x) = ↑(x - x)) = (_ : ↑(x - x) = ↑(x - x))

ink

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

A subgroup of a LinearOrderedCommGroup is a LinearOrderedCommGroup.

Equations

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

ink

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

Equations

• (_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

ink

def AddSubgroupClass.subtype.proof_2 {G : Type u_1} [inst : AddGroup G] {S : Type u_2} (H : S) [inst : SetLike S G] [inst : 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)

Equations

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

ink

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

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

Equations

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

ink

def SubgroupClass.subtype {G : Type u_1} [inst : Group G] {S : Type u_2} (H : S) [inst : SetLike S G] [inst : SubgroupClass S G] : { x // x ∈ H } →* G

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

def AddSubgroupClass.inclusion.proof_2 {G : Type u_1} [inst : AddGroup G] {S : Type u_2} [inst : SetLike S G] [inst : 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)

Equations

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

ink

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

Equations

• (_ : ↑x ∈ K) = h ↑x (_ : ↑x ∈ H)

ink

def AddSubgroupClass.inclusion {G : Type u_1} [inst : AddGroup G] {S : Type u_2} [inst : SetLike S G] [inst : AddSubgroupClass S G] {H : S} {K : S} (h : H ≤ K) : { x // x ∈ H } →+ { x // x ∈ K }

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

Equations

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

ink

def SubgroupClass.inclusion {G : Type u_1} [inst : Group G] {S : Type u_2} [inst : SetLike S G] [inst : 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.

Equations

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

ink

@[simp]

theorem AddSubgroupClass.inclusion_self {G : Type u_1} [inst : AddGroup G] {S : Type u_2} {H : S} [inst : SetLike S G] [inst : AddSubgroupClass S G] (x : { x // x ∈ H }) : ↑(AddSubgroupClass.inclusion (_ : H ≤ H)) x = x

ink

@[simp]

theorem SubgroupClass.inclusion_self {G : Type u_1} [inst : Group G] {S : Type u_2} {H : S} [inst : SetLike S G] [inst : SubgroupClass S G] (x : { x // x ∈ H }) : ↑(SubgroupClass.inclusion (_ : H ≤ H)) x = x

ink

@[simp]

theorem AddSubgroupClass.inclusion_mk {G : Type u_2} [inst : AddGroup G] {S : Type u_1} {H : S} {K : S} [inst : SetLike S G] [inst : AddSubgroupClass S G] {h : H ≤ K} (x : G) (hx : x ∈ H) : ↑(AddSubgroupClass.inclusion h) { val := x, property := hx } = { val := x, property := h x hx }

ink

@[simp]

theorem SubgroupClass.inclusion_mk {G : Type u_2} [inst : Group G] {S : Type u_1} {H : S} {K : S} [inst : SetLike S G] [inst : SubgroupClass S G] {h : H ≤ K} (x : G) (hx : x ∈ H) : ↑(SubgroupClass.inclusion h) { val := x, property := hx } = { val := x, property := h x hx }

ink

theorem AddSubgroupClass.inclusion_right {G : Type u_2} [inst : AddGroup G] {S : Type u_1} {H : S} {K : S} [inst : SetLike S G] [inst : AddSubgroupClass S G] (h : H ≤ K) (x : { x // x ∈ K }) (hx : ↑x ∈ H) : ↑(AddSubgroupClass.inclusion h) { val := ↑x, property := hx } = x

ink

theorem SubgroupClass.inclusion_right {G : Type u_2} [inst : Group G] {S : Type u_1} {H : S} {K : S} [inst : SetLike S G] [inst : SubgroupClass S G] (h : H ≤ K) (x : { x // x ∈ K }) (hx : ↑x ∈ H) : ↑(SubgroupClass.inclusion h) { val := ↑x, property := hx } = x

ink

@[simp]

theorem SubgroupClass.inclusion_inclusion {G : Type u_2} [inst : Group G] {S : Type u_1} {H : S} {K : S} [inst : SetLike S G] [inst : 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

ink

@[simp]

theorem AddSubgroupClass.coe_inclusion {G : Type u_2} [inst : AddGroup G] {S : Type u_1} [inst : SetLike S G] [inst : AddSubgroupClass S G] {H : S} {K : S} {h : H ≤ K} (a : { x // x ∈ H }) : ↑(↑(AddSubgroupClass.inclusion h) a) = ↑a

ink

@[simp]

theorem SubgroupClass.coe_inclusion {G : Type u_2} [inst : Group G] {S : Type u_1} [inst : SetLike S G] [inst : SubgroupClass S G] {H : S} {K : S} {h : H ≤ K} (a : { x // x ∈ H }) : ↑(↑(SubgroupClass.inclusion h) a) = ↑a

ink

@[simp]

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

ink

@[simp]

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

ink

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

• G is closed under inverses

  inv_mem' : ∀ {x : G}, x ∈ toSubmonoid.toSubsemigroup.carrier → x⁻¹ ∈ toSubmonoid.toSubsemigroup.carrier

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

ink

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

• G is closed under negation

  neg_mem' : ∀ {x : G}, x ∈ toAddSubmonoid.toAddSubsemigroup.carrier → -x ∈ toAddSubmonoid.toAddSubsemigroup.carrier

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

ink

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

Equations

• (_ : p = q) = (_ : p = q)

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• (_ : AddSubgroupClass (AddSubgroup G) G) = (_ : AddSubgroupClass (AddSubgroup G) G)

ink

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

Equations

• @AddSubgroup.instAddSubgroupClassAddSubgroupToSubNegAddMonoidInstSetLikeAddSubgroup = @AddSubgroup.instAddSubgroupClassAddSubgroupToSubNegAddMonoidInstSetLikeAddSubgroup.proof_1

ink

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

Equations

• @Subgroup.instSubgroupClassSubgroupToDivInvMonoidInstSetLikeSubgroup = @Subgroup.instSubgroupClassSubgroupToDivInvMonoidInstSetLikeSubgroup.proof_1

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem AddSubgroup.mem_mk {G : Type u_1} [inst : 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

ink

@[simp]

theorem Subgroup.mem_mk {G : Type u_1} [inst : 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

ink

@[simp]

theorem AddSubgroup.coe_set_mk {G : Type u_1} [inst : 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

ink

@[simp]

theorem Subgroup.coe_set_mk {G : Type u_1} [inst : 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

ink

@[simp]

theorem AddSubgroup.mk_le_mk {G : Type u_1} [inst : 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

ink

@[simp]

theorem Subgroup.mk_le_mk {G : Type u_1} [inst : 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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

Conversion to/from Additive/Multiplicative

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

Equations

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

ink

@[inline]

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

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

Equations

• AddSubgroup.toSubgroup' = OrderIso.symm Subgroup.toAddSubgroup

ink

@[simp]

theorem AddSubgroup.toSubgroup_apply_coe {A : Type u_1} [inst : AddGroup A] (S : AddSubgroup A) : ↑(↑(RelIso.toRelEmbedding AddSubgroup.toSubgroup).toEmbedding S) = ↑Multiplicative.toAdd ⁻¹' ↑S

ink

@[simp]

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

ink

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

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

Equations

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

ink

@[inline]

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

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

Equations

• Subgroup.toAddSubgroup' = OrderIso.symm AddSubgroup.toSubgroup

ink

def AddSubgroup.copy.proof_2 {G : Type u_1} [inst : 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

Equations

• (_ : 0 ∈ { carrier := s, add_mem' := (_ : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier) = (_ : 0 ∈ { carrier := s, add_mem' := (_ : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier)

ink

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

Equations

• (_ : a ∈ s → b ∈ s → a + b ∈ s) = (_ : a ∈ s → b ∈ s → a + b ∈ s)

ink

def AddSubgroup.copy.proof_3 {G : Type u_1} [inst : 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

Equations

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

ink

def AddSubgroup.copy {G : Type u_1} [inst : 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

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

ink

def Subgroup.copy {G : Type u_1} [inst : 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

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

theorem AddSubgroup.ext {G : Type u_1} [inst : 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.

ink

theorem Subgroup.ext {G : Type u_1} [inst : 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.

ink

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

An AddSubgroup contains the group's 0.

ink

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

A subgroup contains the group's 1.

ink

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

An AddSubgroup is closed under addition.

ink

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

A subgroup is closed under multiplication.

ink

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

An AddSubgroup is closed under inverse.

ink

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

A subgroup is closed under inverse.

ink

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

An AddSubgroup is closed under subtraction.

ink

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

A subgroup is closed under division.

ink

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

ink

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

ink

theorem AddSubgroup.sub_mem_comm_iff {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {a : G} {b : G} : a - b ∈ H ↔ b - a ∈ H

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

Equations

• AddSubgroup.ofSub.match_1 s motive hsn h_1 = Exists.casesOn hsn fun w h => h_1 w h

ink

def AddSubgroup.ofSub {G : Type u_1} [inst : 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

Equations

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

ink

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

Equations

• (_ : 0 ∈ s) = (_ : 0 ∈ s)

ink

def Subgroup.ofDiv {G : Type u_1} [inst : 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.

Equations

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

ink

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

An AddSubgroup of an AddGroup inherits an addition.

Equations

• AddSubgroup.add H = AddSubmonoid.add H.toAddSubmonoid

ink

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

A subgroup of a group inherits a multiplication.

Equations

• Subgroup.mul H = Submonoid.mul H.toSubmonoid

ink

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

An AddSubgroup of an AddGroup inherits a zero.

Equations

• AddSubgroup.zero H = AddSubmonoid.zero H.toAddSubmonoid

ink

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

A subgroup of a group inherits a 1.

Equations

• Subgroup.one H = Submonoid.one H.toSubmonoid

ink

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

Equations

• (_ : -↑a ∈ H) = (_ : -↑a ∈ H)

ink

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

A AddSubgroup of a AddGroup inherits an inverse.

Equations

• AddSubgroup.neg H = { neg := fun a => { val := -↑a, property := (_ : -↑a ∈ H) } }

ink

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

A subgroup of a group inherits an inverse.

Equations

• Subgroup.inv H = { inv := fun a => { val := (↑a)⁻¹, property := (_ : (↑a)⁻¹ ∈ H) } }

ink

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

Equations

• (_ : ↑a - ↑b ∈ H) = (_ : ↑a - ↑b ∈ H)

ink

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

An AddSubgroup of an AddGroup inherits a subtraction.

Equations

• AddSubgroup.sub H = { sub := fun a b => { val := ↑a - ↑b, property := (_ : ↑a - ↑b ∈ H) } }

ink

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

A subgroup of a group inherits a division

Equations

• Subgroup.div H = { div := fun a b => { val := ↑a / ↑b, property := (_ : ↑a / ↑b ∈ H) } }

ink

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

An AddSubgroup of an AddGroup inherits a natural scaling.

Equations

• AddSubgroup.nsmul = { smul := fun n a => { val := ↑(n • a), property := (_ : n • ↑a ∈ H) } }

ink

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

A subgroup of a group inherits a natural power

Equations

• Subgroup.npow H = { pow := fun a n => { val := ↑(a ^ n), property := (_ : ↑a ^ n ∈ H) } }

ink

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

An AddSubgroup of an AddGroup inherits an integer scaling.

Equations

• AddSubgroup.zsmul = { smul := fun n a => { val := ↑(n • a), property := (_ : n • ↑a ∈ H) } }

ink

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

A subgroup of a group inherits an integer power

Equations

• Subgroup.zpow H = { pow := fun a n => { val := ↑(a ^ n), property := (_ : ↑a ^ n ∈ H) } }

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

• (_ : ↑(-x) = ↑(-x)) = (_ : ↑(-x) = ↑(-x))

ink

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

Equations

• (_ : ↑(x - x) = ↑(x - x)) = (_ : ↑(x - x) = ↑(x - x))

ink

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

Equations

• (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

ink

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

Equations

• (_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

ink

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

An AddSubgroup of an AddGroup inherits an AddGroup structure.

Equations

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

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

A subgroup of a group inherits a group structure.

Equations

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

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

ink

def AddSubgroup.toAddCommGroup.proof_3 {G : Type u_1} [inst : AddCommGroup G] (H : AddSubgroup G) : ∀ (x x_1 : { x // x ∈ H }), ↑(x + x_1) = ↑(x + x_1)

Equations

• (_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

ink

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

Equations

• (_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

ink

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

Equations

• (_ : ↑(-x) = ↑(-x)) = (_ : ↑(-x) = ↑(-x))

ink

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

Equations

• (_ : ↑(x - x) = ↑(x - x)) = (_ : ↑(x - x) = ↑(x - x))

ink

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

An AddSubgroup of an AddCommGroup is an AddCommGroup.

Equations

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

ink

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

A subgroup of a CommGroup is a CommGroup.

Equations

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

ink

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

Equations

• (_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

ink

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

An AddSubgroup of an AddOrderedCommGroup is an AddOrderedCommGroup.

Equations

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

ink

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

Equations

• (_ : ↑(x - x) = ↑(x - x)) = (_ : ↑(x - x) = ↑(x - x))

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ↑(-x) = ↑(-x)) = (_ : ↑(-x) = ↑(-x))

ink

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

Equations

• (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

ink

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

A subgroup of an OrderedCommGroup is an OrderedCommGroup.

Equations

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

ink

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

Equations

• (_ : ↑(-x) = ↑(-x)) = (_ : ↑(-x) = ↑(-x))

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

Equations

• (_ : ↑(x ⊓ x) = ↑(x ⊓ x)) = (_ : ↑(x ⊓ x) = ↑(x ⊓ x))

ink

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

Equations

• (_ : ↑(x ⊔ x) = ↑(x ⊔ x)) = (_ : ↑(x ⊔ x) = ↑(x ⊔ x))

ink

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

Equations

• (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

ink

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

Equations

• (_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

ink

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

Equations

• (_ : ↑(x - x) = ↑(x - x)) = (_ : ↑(x - x) = ↑(x - x))

ink

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

Equations

• (_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

ink

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

Equations

• (_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

ink

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

An AddSubgroup of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

Equations

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

ink

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

A subgroup of a LinearOrderedCommGroup is a LinearOrderedCommGroup.

Equations

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

ink

def AddSubgroup.subtype.proof_2 {G : Type u_1} [inst : 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)

Equations

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

ink

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

Equations

• (_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

ink

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

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

Equations

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

ink

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

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

Equations

• (_ : ↑x ∈ K) = h ↑x (_ : ↑x ∈ H)

ink

def AddSubgroup.inclusion.proof_2 {G : Type u_1} [inst : 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)

Equations

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

ink

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

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

Equations

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

ink

def Subgroup.inclusion {G : Type u_1} [inst : 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.

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

• (_ : -x ∈ Set.univ) = (_ : -x ∈ Set.univ)

ink

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

Equations

• (_ : 0 ∈ ⊤.toAddSubsemigroup.carrier) = (_ : 0 ∈ ⊤.toAddSubsemigroup.carrier)

ink

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

The AddSubgroup G of the AddGroup G.

Equations

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

ink

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

The subgroup G of the group G.

Equations

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

ink

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

The top additive subgroup is isomorphic to the additive group.

This is the additive group version of AddSubmonoid.topEquiv.

Equations

• AddSubgroup.topEquiv = AddSubmonoid.topEquiv

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

The top subgroup is isomorphic to the group.

This is the group version of Submonoid.topEquiv.

Equations

• Subgroup.topEquiv = Submonoid.topEquiv

ink

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

Equations

• (_ : 0 ∈ ⊥.toAddSubsemigroup.carrier) = (_ : 0 ∈ ⊥.toAddSubsemigroup.carrier)

ink

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

Equations

• (_ : ∀ (a : G), a ∈ ⊥.toAddSubsemigroup.carrier → -a ∈ ⊥.toAddSubsemigroup.carrier) = (_ : ∀ (a : G), a ∈ ⊥.toAddSubsemigroup.carrier → -a ∈ ⊥.toAddSubsemigroup.carrier)

ink

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

The trivial AddSubgroup {0} of an AddGroup G.

Equations

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

ink

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

The trivial subgroup {1} of an group G.

Equations

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

ink

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

Equations

• AddSubgroup.instInhabitedAddSubgroup = { default := ⊥ }

ink

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

Equations

• Subgroup.instInhabitedSubgroup = { default := ⊥ }

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

• (_ : g = default) = (_ : g = default)

ink

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

Equations

• AddSubgroup.instUniqueSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupBotInstBotAddSubgroup = { toInhabited := { default := 0 }, uniq := (_ : ∀ (g : { x // x ∈ ⊥ }), g = default) }

ink

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

Equations

• Subgroup.instUniqueSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupBotInstBotSubgroup = { toInhabited := { default := 1 }, uniq := (_ : ∀ (g : { x // x ∈ ⊥ }), g = default) }

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

abbrev AddSubgroup.coe_eq_singleton.match_1 {G : Type u_1} [inst : 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

Equations

• AddSubgroup.coe_eq_singleton.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

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

ink

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

ink

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

ink

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

ink

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

A subgroup is either the trivial subgroup or nontrivial.

ink

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

A subgroup is either the trivial subgroup or nontrivial.

ink

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

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

ink

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

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

ink

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

Equations

• (_ : 0 ∈ (H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid).toAddSubsemigroup.carrier) = (_ : 0 ∈ (H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid).toAddSubsemigroup.carrier)

ink

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

The inf of two add_subgroupss is their intersection.

Equations

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

ink

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

Equations

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

ink

abbrev AddSubgroup.instInfAddSubgroup.match_1 {G : Type u_1} [inst : 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.toAddSubsemigroup.carrier) }.toAddSubsemigroup.carrier → Prop) (x_1 : x ∈ { toAddSubsemigroup := src.toAddSubsemigroup, zero_mem' := (_ : 0 ∈ src.toAddSubsemigroup.carrier) }.toAddSubsemigroup.carrier), (∀ (hx : x ∈ ↑H₁.toAddSubmonoid) (hx' : x ∈ ↑H₂.toAddSubmonoid), motive (_ : x ∈ ↑H₁.toAddSubmonoid ∧ x ∈ ↑H₂.toAddSubmonoid)) → motive x_1

Equations

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

ink

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

The inf of two subgroups is their intersection.

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

def AddSubgroup.instInfSetAddSubgroup.proof_2 {G : Type u_1} [inst : AddGroup G] (s : Set (AddSubgroup G)) : 0 ∈ (AddSubmonoid.copy (⨅ S, ⨅ h, S.toAddSubmonoid) (Set.interᵢ fun S => Set.interᵢ fun h => ↑S) (_ : (Set.interᵢ fun S => Set.interᵢ fun h => ↑S) = ↑(⨅ i, ⨅ h, i.toAddSubmonoid))).toAddSubsemigroup.carrier

Equations

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

ink

def AddSubgroup.instInfSetAddSubgroup.proof_1 {G : Type u_1} [inst : AddGroup G] (s : Set (AddSubgroup G)) : (Set.interᵢ fun S => Set.interᵢ fun h => ↑S) = ↑(⨅ i, ⨅ h, i.toAddSubmonoid)

Equations

• (_ : (Set.interᵢ fun S => Set.interᵢ fun h => ↑S) = ↑(⨅ i, ⨅ h, i.toAddSubmonoid)) = (_ : (Set.interᵢ fun S => Set.interᵢ fun h => ↑S) = ↑(⨅ i, ⨅ h, i.toAddSubmonoid))

ink

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

Equations

• (_ : -x ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x) = (_ : -x ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x)

ink

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

Equations

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

ink

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

Equations

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

ink

@[simp]

theorem AddSubgroup.coe_infₛ {G : Type u_1} [inst : AddGroup G] (H : Set (AddSubgroup G)) : ↑(infₛ H) = Set.interᵢ fun s => Set.interᵢ fun h => ↑s

ink

@[simp]

theorem Subgroup.coe_infₛ {G : Type u_1} [inst : Group G] (H : Set (Subgroup G)) : ↑(infₛ H) = Set.interᵢ fun s => Set.interᵢ fun h => ↑s

ink

@[simp]

theorem AddSubgroup.mem_infₛ {G : Type u_1} [inst : AddGroup G] {S : Set (AddSubgroup G)} {x : G} : x ∈ infₛ S ↔ ∀ (p : AddSubgroup G), p ∈ S → x ∈ p

ink

@[simp]

theorem Subgroup.mem_infₛ {G : Type u_1} [inst : Group G] {S : Set (Subgroup G)} {x : G} : x ∈ infₛ S ↔ ∀ (p : Subgroup G), p ∈ S → x ∈ p

ink

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

ink

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

ink

@[simp]

theorem AddSubgroup.coe_infᵢ {G : Type u_2} [inst : AddGroup G] {ι : Sort u_1} {S : ι → AddSubgroup G} : ↑(⨅ i, S i) = Set.interᵢ fun i => ↑(S i)

ink

@[simp]

theorem Subgroup.coe_infᵢ {G : Type u_2} [inst : Group G] {ι : Sort u_1} {S : ι → Subgroup G} : ↑(⨅ i, S i) = Set.interᵢ fun i => ↑(S i)

ink

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

Equations

• (_ : _x ∈ ↑_a.toAddSubmonoid ∧ _x ∈ ↑_b.toAddSubmonoid → _x ∈ ↑_a.toAddSubmonoid) = (_ : _x ∈ ↑_a.toAddSubmonoid ∧ _x ∈ ↑_b.toAddSubmonoid → _x ∈ ↑_a.toAddSubmonoid)

ink

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

Equations

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

ink

def AddSubgroup.instCompleteLatticeAddSubgroup.proof_1 {G : Type u_1} [inst : AddGroup G] (_s : Set (AddSubgroup G)) : IsGLB _s (infₛ _s)

Equations

• (_ : IsGLB _s (infₛ _s)) = (_ : IsGLB _s (infₛ _s))

ink

def AddSubgroup.instCompleteLatticeAddSubgroup.proof_10 {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G) (_x : G) (hx : _x ∈ ⊥) : _x ∈ S

Equations

• (_ : _x ∈ S) = (_ : _x ∈ S)

ink

def AddSubgroup.instCompleteLatticeAddSubgroup.proof_5 {G : Type u_1} [inst : AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) : a ∈ s → a ≤ supₛ s

Equations

• (_ : ∀ (s : Set (AddSubgroup G)) (a : AddSubgroup G), a ∈ s → a ≤ supₛ s) = (_ : ∀ (