Documentation

Mathlib.GroupTheory.Subgroup.Basic

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:

Definitions in the file:

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_1) (G : Type u_2) [inst : Inv G] [inst : SetLike S G] :
  • s is closed under inverses

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

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

Instances
    class NegMemClass (S : Type u_1) (G : Type u_2) [inst : Neg G] [inst : SetLike S G] :
    • 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.

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

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

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

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

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

              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.

              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
              abbrev zsmul_mem.match_1 (motive : Prop) :
              (x : ) → ((n : ) → motive (Int.ofNat n)) → ((n : ) → motive (Int.negSucc n)) → motive x
              Equations
              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
              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
              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
              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 : GProp} :
              (x, x H P (-x)) x, x H P x
              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 : GProp} :
              (x, x H P x⁻¹) x, x H P x
              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
              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
              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
              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
              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) } }
              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
              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) } }
              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)
              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) } }
              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) } }
              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) } }
              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) } }
              @[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
              @[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)⁻¹
              @[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
              @[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
              def AddSubgroupClass.toAddGroup.proof_2 {G : Type u_2} [inst : AddGroup G] {S : Type u_1} [inst : SetLike S G] [inst : AddSubgroupClass S G] :
              Equations
              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
              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)
              def AddSubgroupClass.toAddGroup.proof_1 {G : Type u_2} [inst : AddGroup G] {S : Type u_1} [inst : SetLike S G] [inst : AddSubgroupClass S G] :
              Equations
              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))
              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
              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))
              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))
              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.
              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
              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.
              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.
              def AddSubgroupClass.toAddCommGroup.proof_2 {S : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst : SetLike S G] [inst : AddSubgroupClass S G] :
              Equations
              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))
              def AddSubgroupClass.toAddCommGroup.proof_1 {S : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst : SetLike S G] [inst : AddSubgroupClass S G] :
              Equations
              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
              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
              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
              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))
              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)
              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))
              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.
              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
              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))
              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)
              instance AddSubgroupClass.toOrderedAddCommGroup {S : Type u_1} (H : S) {G : Type u_2} [inst : OrderedAddCommGroup G] [inst : SetLike S G] [inst : AddSubgroupClass S G] :

              An additive subgroup of an AddOrderedCommGroup is an AddOrderedCommGroup.

              Equations
              • One or more equations did not get rendered due to their size.
              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
              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))
              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))
              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
              def AddSubgroupClass.toOrderedAddCommGroup.proof_1 {S : Type u_1} {G : Type u_2} [inst : OrderedAddCommGroup G] [inst : SetLike S G] [inst : AddSubgroupClass S G] :
              Equations
              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.
              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
              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
              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))
              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
              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))
              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)
              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
              instance AddSubgroupClass.toLinearOrderedAddCommGroup {S : Type u_1} (H : S) {G : Type u_2} [inst : LinearOrderedAddCommGroup G] [inst : SetLike S G] [inst : AddSubgroupClass S G] :

              An additive subgroup of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

              Equations
              • One or more equations did not get rendered due to their size.
              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
              Equations
              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))
              instance SubgroupClass.toLinearOrderedCommGroup {S : Type u_1} (H : S) {G : Type u_2} [inst : LinearOrderedCommGroup G] [inst : SetLike S G] [inst : SubgroupClass S G] :

              A subgroup of a LinearOrderedCommGroup is a LinearOrderedCommGroup.

              Equations
              • One or more equations did not get rendered due to their size.
              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)
              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.
              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.
              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.
              @[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
              @[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
              @[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
              @[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
              @[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
              @[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
              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.
              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)
              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.
              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.
              @[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
              @[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
              @[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 }
              @[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 }
              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
              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
              @[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 }) :
              @[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
              @[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
              @[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) :
              @[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) :
              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.carrierx⁻¹ toSubmonoid.toSubsemigroup.carrier

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

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

                Instances For
                  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)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  instance Subgroup.instSetLikeSubgroup {G : Type u_1} [inst : Group G] :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  @[simp]
                  theorem AddSubgroup.mem_carrier {G : Type u_1} [inst : AddGroup G] {s : AddSubgroup G} {x : G} :
                  x s.toAddSubmonoid.toAddSubsemigroup.carrier x s
                  @[simp]
                  theorem Subgroup.mem_carrier {G : Type u_1} [inst : Group G] {s : Subgroup G} {x : G} :
                  x s.toSubmonoid.toSubsemigroup.carrier x s
                  @[simp]
                  theorem AddSubgroup.mem_mk {G : Type u_1} [inst : AddGroup G] {s : Set G} {x : G} (h_one : ∀ {a b : G}, a sb sa + 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} [inst : Group G] {s : Set G} {x : G} (h_one : ∀ {a b : G}, a sb sa * b s) (h_mul : s 1) (h_inv : ∀ {x : G}, x { toSubsemigroup := { carrier := s, mul_mem' := h_one }, one_mem' := h_mul }.toSubsemigroup.carrierx⁻¹ { 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} [inst : AddGroup G] {s : Set G} (h_one : ∀ {a b : G}, a sb sa + 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} [inst : Group G] {s : Set G} (h_one : ∀ {a b : G}, a sb sa * b s) (h_mul : s 1) (h_inv : ∀ {x : G}, x { toSubsemigroup := { carrier := s, mul_mem' := h_one }, one_mem' := h_mul }.toSubsemigroup.carrierx⁻¹ { 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} [inst : AddGroup G] {s : Set G} {t : Set G} (h_one : ∀ {a b : G}, a sb sa + 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 tb ta + 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} [inst : Group G] {s : Set G} {t : Set G} (h_one : ∀ {a b : G}, a sb sa * b s) (h_mul : s 1) (h_inv : ∀ {x : G}, x { toSubsemigroup := { carrier := s, mul_mem' := h_one }, one_mem' := h_mul }.toSubsemigroup.carrierx⁻¹ { toSubsemigroup := { carrier := s, mul_mem' := h_one }, one_mem' := h_mul }.toSubsemigroup.carrier) (h_one' : ∀ {a b : G}, a tb ta * b t) (h_mul' : t 1) (h_inv' : ∀ {x : G}, x { toSubsemigroup := { carrier := t, mul_mem' := h_one' }, one_mem' := h_mul' }.toSubsemigroup.carrierx⁻¹ { 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} [inst : AddGroup G] (K : AddSubgroup G) :
                  K.toAddSubmonoid = K
                  @[simp]
                  theorem Subgroup.coe_toSubmonoid {G : Type u_1} [inst : Group G] (K : Subgroup G) :
                  K.toSubmonoid = K
                  @[simp]
                  theorem AddSubgroup.mem_toAddSubmonoid {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) (x : G) :
                  x K.toAddSubmonoid x K
                  @[simp]
                  theorem Subgroup.mem_toSubmonoid {G : Type u_1} [inst : Group G] (K : Subgroup G) (x : G) :
                  x K.toSubmonoid x K
                  theorem AddSubgroup.toAddSubmonoid_injective {G : Type u_1} [inst : AddGroup G] :
                  Function.Injective AddSubgroup.toAddSubmonoid
                  theorem Subgroup.toSubmonoid_injective {G : Type u_1} [inst : Group G] :
                  Function.Injective Subgroup.toSubmonoid
                  @[simp]
                  theorem AddSubgroup.toAddSubmonoid_eq {G : Type u_1} [inst : AddGroup G] {p : AddSubgroup G} {q : AddSubgroup G} :
                  p.toAddSubmonoid = q.toAddSubmonoid p = q
                  @[simp]
                  theorem Subgroup.toSubmonoid_eq {G : Type u_1} [inst : Group G] {p : Subgroup G} {q : Subgroup G} :
                  p.toSubmonoid = q.toSubmonoid p = q
                  theorem AddSubgroup.toAddSubmonoid_strictMono {G : Type u_1} [inst : AddGroup G] :
                  StrictMono AddSubgroup.toAddSubmonoid
                  theorem Subgroup.toSubmonoid_strictMono {G : Type u_1} [inst : Group G] :
                  StrictMono Subgroup.toSubmonoid
                  theorem AddSubgroup.toAddSubmonoid_mono {G : Type u_1} [inst : AddGroup G] :
                  Monotone AddSubgroup.toAddSubmonoid
                  theorem Subgroup.toSubmonoid_mono {G : Type u_1} [inst : Group G] :
                  Monotone Subgroup.toSubmonoid
                  @[simp]
                  theorem AddSubgroup.toAddSubmonoid_le {G : Type u_1} [inst : AddGroup G] {p : AddSubgroup G} {q : AddSubgroup G} :
                  p.toAddSubmonoid q.toAddSubmonoid p q
                  @[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 #

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

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

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

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

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

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

                  Equations
                  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 sb sa + b s) }.carrier
                  Equations
                  • (_ : 0 { carrier := s, add_mem' := (_ : ∀ {a b : G}, a sb sa + b s) }.carrier) = (_ : 0 { carrier := s, add_mem' := (_ : ∀ {a b : G}, a sb sa + b s) }.carrier)
                  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 sb sa + b s
                  Equations
                  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 sb sa + b s) }, zero_mem' := (_ : 0 { carrier := s, add_mem' := (_ : ∀ {a b : G}, a sb sa + b s) }.carrier) }.toAddSubsemigroup.carrier-x { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : G}, a sb sa + b s) }, zero_mem' := (_ : 0 { carrier := s, add_mem' := (_ : ∀ {a b : G}, a sb sa + b s) }.carrier) }.toAddSubsemigroup.carrier
                  Equations
                  • One or more equations did not get rendered due to their size.
                  def AddSubgroup.copy {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :

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

                  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.
                  @[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
                  @[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
                  theorem AddSubgroup.copy_eq {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :
                  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
                  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.

                  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.

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

                  An AddSubgroup contains the group's 0.

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

                  A subgroup contains the group's 1.

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

                  An AddSubgroup is closed under addition.

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

                  A subgroup is closed under multiplication.

                  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.

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

                  A subgroup is closed under inverse.

                  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.

                  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.

                  theorem AddSubgroup.neg_mem_iff {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x : G} :
                  -x H x H
                  theorem Subgroup.inv_mem_iff {G : Type u_1} [inst : Group G] (H : Subgroup G) {x : G} :
                  x⁻¹ H x H
                  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
                  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
                  theorem AddSubgroup.exists_neg_mem_iff_exists_mem {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {P : GProp} :
                  (x, x K P (-x)) x, x K P x
                  theorem Subgroup.exists_inv_mem_iff_exists_mem {G : Type u_1} [inst : Group G] (K : Subgroup G) {P : GProp} :
                  (x, x K P x⁻¹) x, x K P x
                  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
                  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
                  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
                  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
                  theorem AddSubgroup.nsmul_mem {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {x : G} (hx : x K) (n : ) :
                  n x K
                  theorem Subgroup.pow_mem {G : Type u_1} [inst : Group G] (K : Subgroup G) {x : G} (hx : x K) (n : ) :
                  x ^ n K
                  theorem AddSubgroup.zsmul_mem {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {x : G} (hx : x K) (n : ) :
                  n x K
                  theorem Subgroup.zpow_mem {G : Type u_1} [inst : Group G] (K : Subgroup G) {x : G} (hx : x K) (n : ) :
                  x ^ n K
                  abbrev AddSubgroup.ofSub.match_1 {G : Type u_1} (s : Set G) (motive : Set.Nonempty sProp) :
                  (hsn : Set.Nonempty s) → ((x : G) → (hx : x s) → motive (_ : x, x s)) → motive hsn
                  Equations
                  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 sx + -y s) :

                  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.
                  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 sx + -y s) :
                  0 s
                  Equations
                  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 sx * y⁻¹ s) :

                  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.
                  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
                  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
                  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
                  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
                  def AddSubgroup.neg.proof_1 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (a : { x // x H }) :
                  -a H
                  Equations
                  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
                  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
                  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)
                  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
                  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) } }
                  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) } }
                  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) } }
                  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) } }
                  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) } }
                  @[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
                  @[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
                  @[simp]
                  theorem AddSubgroup.coe_zero {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) :
                  0 = 0
                  @[simp]
                  theorem Subgroup.coe_one {G : Type u_1} [inst : Group G] (H : Subgroup G) :
                  1 = 1
                  @[simp]
                  theorem AddSubgroup.coe_neg {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (x : { x // x H }) :
                  ↑(-x) = -x
                  @[simp]
                  theorem Subgroup.coe_inv {G : Type u_1} [inst : Group G] (H : Subgroup G) (x : { x // x H }) :
                  x⁻¹ = (x)⁻¹
                  @[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
                  @[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
                  theorem AddSubgroup.coe_mk {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (x : G) (hx : x H) :
                  { val := x, property := hx } = x
                  theorem Subgroup.coe_mk {G : Type u_1} [inst : Group G] (H : Subgroup G) (x : G) (hx : x H) :
                  { val := x, property := hx } = x
                  @[simp]
                  theorem AddSubgroup.coe_nsmul {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (x : { x // x H }) (n : ) :
                  ↑(n x) = n x
                  @[simp]
                  theorem Subgroup.coe_pow {G : Type u_1} [inst : Group G] (H : Subgroup G) (x : { x // x H }) (n : ) :
                  ↑(x ^ n) = x ^ n
                  theorem AddSubgroup.coe_zsmul {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (x : { x // x H }) (n : ) :
                  ↑(n x) = n x
                  theorem Subgroup.coe_zpow {G : Type u_1} [inst : 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} [inst : 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} [inst : Group G] (H : Subgroup G) {g : G} {h : g H} :
                  { val := g, property := h } = 1 g = 1
                  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))
                  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))
                  def AddSubgroup.toAddGroup.proof_1 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) :
                  Function.Injective fun a => a
                  Equations
                  def AddSubgroup.toAddGroup.proof_2 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) :
                  0 = 0
                  Equations
                  • (_ : 0 = 0) = (_ : 0 = 0)
                  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.
                  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
                  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))
                  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
                  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.
                  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
                  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
                  Equations
                  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))
                  def AddSubgroup.toAddCommGroup.proof_2 {G : Type u_1} [inst : AddCommGroup G] (H : AddSubgroup G) :
                  0 = 0
                  Equations
                  • (_ : 0 = 0) = (_ : 0 = 0)
                  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))
                  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))
                  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.
                  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.
                  Equations
                  • (_ : 0 = 0) = (_ : 0 = 0)

                  An AddSubgroup of an AddOrderedCommGroup is an AddOrderedCommGroup.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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))
                  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
                  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))
                  Equations
                  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
                  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))
                  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.
                  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))
                  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
                  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
                  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
                  Equations
                  Equations
                  • (_ : 0 = 0) = (_ : 0 = 0)
                  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))
                  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))
                  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

                  An AddSubgroup of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

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

                  A subgroup of a LinearOrderedCommGroup is a LinearOrderedCommGroup.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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.
                  def AddSubgroup.subtype.proof_1 {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) :
                  0 = 0
                  Equations
                  • (_ : 0 = 0) = (_ : 0 = 0)
                  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.
                  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.
                  @[simp]
                  theorem AddSubgroup.coeSubtype {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) :
                  ↑(AddSubgroup.subtype H) = Subtype.val
                  @[simp]
                  theorem Subgroup.coeSubtype {G : Type u_1} [inst : Group G] (H : Subgroup G) :
                  ↑(Subgroup.subtype H) = Subtype.val
                  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)
                  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.
                  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.
                  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.
                  @[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
                  @[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
                  theorem Subgroup.inclusion_injective {G : Type u_1} [inst : Group G] {H : Subgroup G} {K : Subgroup G} (h : H K) :
                  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)
                  def AddSubgroup.instTopAddSubgroup.proof_1 {G : Type u_1} [inst : AddGroup G] :
                  0 .toAddSubsemigroup.carrier
                  Equations
                  • (_ : 0 .toAddSubsemigroup.carrier) = (_ : 0 .toAddSubsemigroup.carrier)
                  instance AddSubgroup.instTopAddSubgroup {G : Type u_1} [inst : AddGroup G] :

                  The AddSubgroup G of the AddGroup G.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  instance Subgroup.instTopSubgroup {G : Type u_1} [inst : Group G] :

                  The subgroup G of the group G.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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
                  @[simp]
                  theorem AddSubgroup.topEquiv_apply {G : Type u_1} [inst : AddGroup G] (x : { x // x }) :
                  AddSubgroup.topEquiv x = x
                  @[simp]
                  theorem Subgroup.topEquiv_symm_apply_coe {G : Type u_1} [inst : Group G] (x : G) :
                  ↑(↑(MulEquiv.symm Subgroup.topEquiv) x) = x
                  @[simp]
                  theorem Subgroup.topEquiv_apply {G : Type u_1} [inst : Group G] (x : { x // x }) :
                  Subgroup.topEquiv x = x
                  @[simp]
                  theorem AddSubgroup.topEquiv_symm_apply_coe {G : Type u_1} [inst : AddGroup G] (x : G) :
                  ↑(↑(AddEquiv.symm AddSubgroup.topEquiv) x) = x
                  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
                  def AddSubgroup.instBotAddSubgroup.proof_1 {G : Type u_1} [inst : AddGroup G] :
                  0 .toAddSubsemigroup.carrier
                  Equations
                  • (_ : 0 .toAddSubsemigroup.carrier) = (_ : 0 .toAddSubsemigroup.carrier)
                  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)
                  instance AddSubgroup.instBotAddSubgroup {G : Type u_1} [inst : AddGroup G] :

                  The trivial AddSubgroup {0} of an AddGroup G.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  instance Subgroup.instBotSubgroup {G : Type u_1} [inst : Group G] :

                  The trivial subgroup {1} of an group G.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Equations
                  • AddSubgroup.instInhabitedAddSubgroup = { default := }
                  instance Subgroup.instInhabitedSubgroup {G : Type u_1} [inst : Group G] :
                  Equations
                  • Subgroup.instInhabitedSubgroup = { default := }
                  @[simp]
                  theorem AddSubgroup.mem_bot {G : Type u_1} [inst : AddGroup G] {x : G} :
                  x x = 0
                  @[simp]
                  theorem Subgroup.mem_bot {G : Type u_1} [inst : Group G] {x : G} :
                  x x = 1
                  @[simp]
                  theorem AddSubgroup.mem_top {G : Type u_1} [inst : AddGroup G] (x : G) :
                  @[simp]
                  theorem Subgroup.mem_top {G : Type u_1} [inst : Group G] (x : G) :
                  @[simp]
                  theorem AddSubgroup.coe_top {G : Type u_1} [inst : AddGroup G] :
                  = Set.univ
                  @[simp]
                  theorem Subgroup.coe_top {G : Type u_1} [inst : Group G] :
                  = Set.univ
                  @[simp]
                  theorem AddSubgroup.coe_bot {G : Type u_1} [inst : AddGroup G] :
                  = {0}
                  @[simp]
                  theorem Subgroup.coe_bot {G : Type u_1} [inst : Group G] :
                  = {1}
                  Equations
                  • (_ : g = default) = (_ : g = default)
                  Equations
                  • AddSubgroup.instUniqueSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupBotInstBotAddSubgroup = { toInhabited := { default := 0 }, uniq := (_ : ∀ (g : { x // x }), g = default) }
                  Equations
                  • Subgroup.instUniqueSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupBotInstBotSubgroup = { toInhabited := { default := 1 }, uniq := (_ : ∀ (g : { x // x }), g = default) }
                  @[simp]
                  theorem AddSubgroup.top_toAddSubmonoid {G : Type u_1} [inst : AddGroup G] :
                  .toAddSubmonoid =
                  @[simp]
                  theorem Subgroup.top_toSubmonoid {G : Type u_1} [inst : Group G] :
                  .toSubmonoid =
                  @[simp]
                  theorem AddSubgroup.bot_toAddSubmonoid {G : Type u_1} [inst : AddGroup G] :
                  .toAddSubmonoid =
                  @[simp]
                  theorem Subgroup.bot_toSubmonoid {G : Type u_1} [inst : Group G] :
                  .toSubmonoid =
                  theorem AddSubgroup.eq_bot_iff_forall {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) :
                  H = ∀ (x : G), x Hx = 0
                  theorem Subgroup.eq_bot_iff_forall {G : Type u_1} [inst : Group G] (H : Subgroup G) :
                  H = ∀ (x : G), x Hx = 1
                  theorem AddSubgroup.eq_bot_of_subsingleton {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst : Subsingleton { x // x H }] :
                  H =
                  theorem Subgroup.eq_bot_of_subsingleton {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst : Subsingleton { x // x H }] :
                  H =
                  theorem AddSubgroup.coe_eq_univ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} :
                  H = Set.univ H =
                  theorem Subgroup.coe_eq_univ {G : Type u_1} [inst : Group G] {H : Subgroup G} :
                  H = Set.univ H =
                  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
                  theorem AddSubgroup.coe_eq_singleton {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} :
                  (g, H = {g}) H =
                  theorem Subgroup.coe_eq_singleton {G : Type u_1} [inst : Group G] {H : Subgroup G} :
                  (g, H = {g}) H =
                  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
                  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
                  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.

                  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.

                  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.

                  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.

                  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)
                  instance AddSubgroup.instInfAddSubgroup {G : Type u_1} [inst : AddGroup G] :

                  The inf of two add_subgroupss is their intersection.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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.
                  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.carrierProp) (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.
                  instance Subgroup.instInfSubgroup {G : Type u_1} [inst : Group G] :

                  The inf of two subgroups is their intersection.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  @[simp]
                  theorem AddSubgroup.coe_inf {G : Type u_1} [inst : AddGroup G] (p : AddSubgroup G) (p' : AddSubgroup G) :
                  ↑(p p') = p p'
                  @[simp]
                  theorem Subgroup.coe_inf {G : Type u_1} [inst : Group G] (p : Subgroup G) (p' : Subgroup G) :
                  ↑(p p') = p p'
                  @[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'
                  @[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'
                  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.
                  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
                  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
                  Equations
                  • One or more equations did not get rendered due to their size.
                  instance Subgroup.instInfSetSubgroup {G : Type u_1} [inst : Group G] :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  @[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
                  @[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
                  @[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 Sx p
                  @[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 Sx p
                  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
                  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
                  @[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)
                  @[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)
                  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)
                  def AddSubgroup.instCompleteLatticeAddSubgroup.proof_8 {G : Type u_1} [inst : AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) :
                  (∀ (b : AddSubgroup G), b sa b) → a infₛ s
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Equations
                  def AddSubgroup.instCompleteLatticeAddSubgroup.proof_10 {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G) (_x : G) (hx : _x ) :
                  _x S
                  Equations
                  Equations