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_5) (G : Type u_6) [Inv G] [SetLike S G] :

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

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

    s is closed under inverses

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

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

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

      s is closed under negation

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

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

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

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

            Instances
              @[simp]
              theorem neg_mem_iff {S : Type u_5} {G : Type u_6} [InvolutiveNeg G] :
              ∀ {x : SetLike S G} [inst : NegMemClass S G] {H : S} {x_1 : G}, -x_1 H x_1 H
              @[simp]
              theorem inv_mem_iff {S : Type u_5} {G : Type u_6} [InvolutiveInv G] :
              ∀ {x : SetLike S G} [inst : InvMemClass S G] {H : S} {x_1 : G}, x_1⁻¹ H x_1 H
              @[simp]
              theorem abs_mem_iff {S : Type u_5} {G : Type u_6} [AddGroup G] [LinearOrder G] :
              ∀ {x : SetLike S G} [inst : NegMemClass S G] {H : S} {x_1 : G}, |x_1| H x_1 H
              theorem sub_mem {M : Type u_5} {S : Type u_6} [SubNegMonoid M] [SetLike S M] [hSM : AddSubgroupClass S M] {H : S} {x : M} {y : M} (hx : x H) (hy : y H) :
              x - y H

              An additive subgroup is closed under subtraction.

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

              A subgroup is closed under division.

              abbrev zsmul_mem.match_1 (motive : Prop) :
              ∀ (x : ), (∀ (n : ), motive (Int.ofNat n))(∀ (n : ), motive (Int.negSucc n))motive x
              Equations
              • (_ : motive x) = (_ : motive x)
              Instances For
                theorem zsmul_mem {M : Type u_5} {S : Type u_6} [SubNegMonoid M] [SetLike S M] [hSM : AddSubgroupClass S M] {K : S} {x : M} (hx : x K) (n : ) :
                n x K
                theorem zpow_mem {M : Type u_5} {S : Type u_6} [DivInvMonoid M] [SetLike S M] [hSM : SubgroupClass S M] {K : S} {x : M} (hx : x K) (n : ) :
                x ^ n K
                theorem sub_mem_comm_iff {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] {a : G} {b : G} :
                a - b H b - a H
                theorem div_mem_comm_iff {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] {a : G} {b : G} :
                a / b H b / a H
                theorem exists_neg_mem_iff_exists_mem {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] {P : GProp} :
                (∃ x ∈ H, P (-x)) ∃ x ∈ H, P x
                theorem exists_inv_mem_iff_exists_mem {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] {P : GProp} :
                (∃ x ∈ H, P x⁻¹) ∃ x ∈ H, P x
                theorem add_mem_cancel_right {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] {x : G} {y : G} (h : x H) :
                y + x H y H
                theorem mul_mem_cancel_right {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] {x : G} {y : G} (h : x H) :
                y * x H y H
                theorem add_mem_cancel_left {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] {x : G} {y : G} (h : x H) :
                x + y H y H
                theorem mul_mem_cancel_left {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] {x : G} {y : G} (h : x H) :
                x * y H y H
                theorem NegMemClass.neg.proof_1 {G : Type u_1} {S : Type u_2} [Neg G] [SetLike S G] [NegMemClass S G] {H : S} (a : H) :
                -a H
                instance NegMemClass.neg {G : Type u_1} {S : Type u_2} [Neg G] [SetLike S G] [NegMemClass S G] {H : S} :
                Neg H

                An additive subgroup of an AddGroup inherits an inverse.

                Equations
                • NegMemClass.neg = { neg := fun (a : H) => { val := -a, property := (_ : -a H) } }
                instance InvMemClass.inv {G : Type u_1} {S : Type u_2} [Inv G] [SetLike S G] [InvMemClass S G] {H : S} :
                Inv H

                A subgroup of a group inherits an inverse.

                Equations
                • InvMemClass.inv = { inv := fun (a : H) => { val := (a)⁻¹, property := (_ : (a)⁻¹ H) } }
                @[simp]
                theorem NegMemClass.coe_neg {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : H) :
                (-x) = -x
                @[simp]
                theorem InvMemClass.coe_inv {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] (x : H) :
                x⁻¹ = (x)⁻¹
                @[deprecated]
                theorem SubgroupClass.coe_inv {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] (x : H) :
                x⁻¹ = (x)⁻¹

                Alias of InvMemClass.coe_inv.

                @[deprecated]
                theorem AddSubgroupClass.coe_neg {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : H) :
                (-x) = -x
                abbrev AddSubgroupClass.subset_union.match_1 {G : Type u_1} {S : Type u_2} [SetLike S G] {H : S} {K : S} (motive : (∃ x ∈ H, xK)Prop) :
                ∀ (x : ∃ x ∈ H, xK), (∀ (x : G) (xH : x H) (xK : xK), motive (_ : ∃ x ∈ H, xK))motive x
                Equations
                • (_ : motive x) = (_ : motive x)
                Instances For
                  theorem AddSubgroupClass.subset_union {G : Type u_1} [AddGroup G] {S : Type u_6} [SetLike S G] [AddSubgroupClass S G] {H : S} {K : S} {L : S} :
                  H K L H K H L
                  theorem SubgroupClass.subset_union {G : Type u_1} [Group G] {S : Type u_6} [SetLike S G] [SubgroupClass S G] {H : S} {K : S} {L : S} :
                  H K L H K H L
                  theorem AddSubgroupClass.sub.proof_1 {G : Type u_1} {S : Type u_2} [SubNegMonoid G] [SetLike S G] [AddSubgroupClass S G] {H : S} (a : H) (b : H) :
                  a - b H
                  instance AddSubgroupClass.sub {G : Type u_1} {S : Type u_2} [SubNegMonoid G] [SetLike S G] [AddSubgroupClass S G] {H : S} :
                  Sub H

                  An additive subgroup of an AddGroup inherits a subtraction.

                  Equations
                  • AddSubgroupClass.sub = { sub := fun (a b : H) => { val := a - b, property := (_ : a - b H) } }
                  instance SubgroupClass.div {G : Type u_1} {S : Type u_2} [DivInvMonoid G] [SetLike S G] [SubgroupClass S G] {H : S} :
                  Div H

                  A subgroup of a group inherits a division

                  Equations
                  • SubgroupClass.div = { div := fun (a b : H) => { val := a / b, property := (_ : a / b H) } }
                  instance AddSubgroupClass.zsmul {M : Type u_7} {S : Type u_8} [SubNegMonoid M] [SetLike S M] [AddSubgroupClass S M] {H : S} :
                  SMul H

                  An additive subgroup of an AddGroup inherits an integer scaling.

                  Equations
                  • AddSubgroupClass.zsmul = { smul := fun (n : ) (a : H) => { val := n a, property := (_ : n a H) } }
                  instance SubgroupClass.zpow {M : Type u_7} {S : Type u_8} [DivInvMonoid M] [SetLike S M] [SubgroupClass S M] {H : S} :
                  Pow H

                  A subgroup of a group inherits an integer power.

                  Equations
                  • SubgroupClass.zpow = { pow := fun (a : H) (n : ) => { val := a ^ n, property := (_ : a ^ n H) } }
                  @[simp]
                  theorem AddSubgroupClass.coe_sub {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : H) (y : H) :
                  (x - y) = x - y
                  @[simp]
                  theorem SubgroupClass.coe_div {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] (x : H) (y : H) :
                  (x / y) = x / y
                  theorem AddSubgroupClass.toAddGroup.proof_4 {G : Type u_1} {S : Type u_2} (H : S) [SetLike S G] :
                  Function.Injective fun (a : H) => a
                  theorem AddSubgroupClass.toAddGroup.proof_10 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                  ∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
                  theorem AddSubgroupClass.toAddGroup.proof_8 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                  ∀ (x x_1 : H), (x - x_1) = (x - x_1)
                  theorem AddSubgroupClass.toAddGroup.proof_6 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                  ∀ (x x_1 : H), (x + x_1) = (x + x_1)
                  theorem AddSubgroupClass.toAddGroup.proof_9 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                  ∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
                  theorem AddSubgroupClass.toAddGroup.proof_5 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                  0 = 0
                  theorem AddSubgroupClass.toAddGroup.proof_7 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                  ∀ (x : H), (-x) = (-x)
                  instance AddSubgroupClass.toAddGroup {G : Type u_1} [AddGroup G] {S : Type u_6} (H : S) [SetLike S G] [AddSubgroupClass S G] :

                  An additive subgroup of an AddGroup inherits an AddGroup structure.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  instance SubgroupClass.toGroup {G : Type u_1} [Group G] {S : Type u_6} (H : S) [SetLike S G] [SubgroupClass S G] :
                  Group H

                  A subgroup of a group inherits a group structure.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  theorem AddSubgroupClass.toAddCommGroup.proof_8 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
                  ∀ (x x_1 : H), (x - x_1) = (x - x_1)
                  theorem AddSubgroupClass.toAddCommGroup.proof_5 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
                  0 = 0
                  theorem AddSubgroupClass.toAddCommGroup.proof_9 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
                  ∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
                  theorem AddSubgroupClass.toAddCommGroup.proof_10 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
                  ∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
                  theorem AddSubgroupClass.toAddCommGroup.proof_7 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
                  ∀ (x : H), (-x) = (-x)
                  theorem AddSubgroupClass.toAddCommGroup.proof_6 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
                  ∀ (x x_1 : H), (x + x_1) = (x + x_1)
                  instance AddSubgroupClass.toAddCommGroup {S : Type u_6} (H : S) {G : Type u_7} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :

                  An additive subgroup of an AddCommGroup is an AddCommGroup.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  theorem AddSubgroupClass.toAddCommGroup.proof_4 {S : Type u_2} (H : S) {G : Type u_1} [SetLike S G] :
                  Function.Injective fun (a : H) => a
                  instance SubgroupClass.toCommGroup {S : Type u_6} (H : S) {G : Type u_7} [CommGroup G] [SetLike S G] [SubgroupClass S G] :

                  A subgroup of a CommGroup is a CommGroup.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  theorem AddSubgroupClass.subtype.proof_2 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                  ∀ (x x_1 : H), { toFun := Subtype.val, map_zero' := (_ : 0 = 0) }.toFun (x + x_1) = { toFun := Subtype.val, map_zero' := (_ : 0 = 0) }.toFun (x + x_1)
                  def AddSubgroupClass.subtype {G : Type u_1} [AddGroup G] {S : Type u_6} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                  H →+ G

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem AddSubgroupClass.subtype.proof_1 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                    0 = 0
                    def SubgroupClass.subtype {G : Type u_1} [Group G] {S : Type u_6} (H : S) [SetLike S G] [SubgroupClass S G] :
                    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.
                    Instances For
                      @[simp]
                      theorem AddSubgroupClass.coeSubtype {G : Type u_1} [AddGroup G] {S : Type u_6} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                      H = Subtype.val
                      @[simp]
                      theorem SubgroupClass.coeSubtype {G : Type u_1} [Group G] {S : Type u_6} (H : S) [SetLike S G] [SubgroupClass S G] :
                      H = Subtype.val
                      @[simp]
                      theorem AddSubgroupClass.coe_nsmul {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : H) (n : ) :
                      (n x) = n x
                      @[simp]
                      theorem SubgroupClass.coe_pow {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] (x : H) (n : ) :
                      (x ^ n) = x ^ n
                      @[simp]
                      theorem AddSubgroupClass.coe_zsmul {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : H) (n : ) :
                      (n x) = n x
                      @[simp]
                      theorem SubgroupClass.coe_zpow {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] (x : H) (n : ) :
                      (x ^ n) = x ^ n
                      def AddSubgroupClass.inclusion {G : Type u_1} [AddGroup G] {S : Type u_6} [SetLike S G] [AddSubgroupClass S G] {H : S} {K : S} (h : H K) :
                      H →+ K

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem AddSubgroupClass.inclusion.proof_2 {G : Type u_1} [AddGroup G] {S : Type u_2} [SetLike S G] [AddSubgroupClass S G] {H : S} {K : S} (h : H K) :
                        ∀ (x x_1 : H), (fun (x : H) => { val := x, property := (_ : x K) }) (x + x_1) = (fun (x : H) => { val := x, property := (_ : x K) }) (x + x_1)
                        theorem AddSubgroupClass.inclusion.proof_1 {G : Type u_1} {S : Type u_2} [SetLike S G] {H : S} {K : S} (h : H K) (x : H) :
                        x K
                        def SubgroupClass.inclusion {G : Type u_1} [Group G] {S : Type u_6} [SetLike S G] [SubgroupClass S G] {H : S} {K : S} (h : H K) :
                        H →* K

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem AddSubgroupClass.inclusion_self {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : H) :
                          @[simp]
                          theorem SubgroupClass.inclusion_self {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] (x : H) :
                          (SubgroupClass.inclusion (_ : H H)) x = x
                          @[simp]
                          theorem AddSubgroupClass.inclusion_mk {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} {K : S} [SetLike S G] [AddSubgroupClass S G] {h : H K} (x : G) (hx : x H) :
                          (AddSubgroupClass.inclusion h) { val := x, property := hx } = { val := x, property := (_ : x K) }
                          @[simp]
                          theorem SubgroupClass.inclusion_mk {G : Type u_1} [Group G] {S : Type u_6} {H : S} {K : S} [SetLike S G] [SubgroupClass S G] {h : H K} (x : G) (hx : x H) :
                          (SubgroupClass.inclusion h) { val := x, property := hx } = { val := x, property := (_ : x K) }
                          theorem AddSubgroupClass.inclusion_right {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} {K : S} [SetLike S G] [AddSubgroupClass S G] (h : H K) (x : K) (hx : x H) :
                          (AddSubgroupClass.inclusion h) { val := x, property := hx } = x
                          theorem SubgroupClass.inclusion_right {G : Type u_1} [Group G] {S : Type u_6} {H : S} {K : S} [SetLike S G] [SubgroupClass S G] (h : H K) (x : K) (hx : x H) :
                          (SubgroupClass.inclusion h) { val := x, property := hx } = x
                          @[simp]
                          theorem SubgroupClass.inclusion_inclusion {G : Type u_1} [Group G] {S : Type u_6} {H : S} {K : S} [SetLike S G] [SubgroupClass S G] {L : S} (hHK : H K) (hKL : K L) (x : H) :
                          @[simp]
                          theorem AddSubgroupClass.coe_inclusion {G : Type u_1} [AddGroup G] {S : Type u_6} [SetLike S G] [AddSubgroupClass S G] {H : S} {K : S} {h : H K} (a : H) :
                          @[simp]
                          theorem SubgroupClass.coe_inclusion {G : Type u_1} [Group G] {S : Type u_6} [SetLike S G] [SubgroupClass S G] {H : S} {K : S} {h : H K} (a : H) :
                          ((SubgroupClass.inclusion h) a) = a
                          @[simp]
                          theorem AddSubgroupClass.subtype_comp_inclusion {G : Type u_1} [AddGroup G] {S : Type u_6} [SetLike S G] [AddSubgroupClass S G] {H : S} {K : S} (hH : H K) :
                          @[simp]
                          theorem SubgroupClass.subtype_comp_inclusion {G : Type u_1} [Group G] {S : Type u_6} [SetLike S G] [SubgroupClass S G] {H : S} {K : S} (hH : H K) :
                          structure Subgroup (G : Type u_5) [Group G] extends Submonoid :
                          Type u_5

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

                          • carrier : Set G
                          • mul_mem' : ∀ {a b : G}, a self.carrierb self.carriera * b self.carrier
                          • one_mem' : 1 self.carrier
                          • inv_mem' : ∀ {x : G}, x self.carrierx⁻¹ self.carrier

                            G is closed under inverses

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

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

                            • carrier : Set G
                            • add_mem' : ∀ {a b : G}, a self.carrierb self.carriera + b self.carrier
                            • zero_mem' : 0 self.carrier
                            • neg_mem' : ∀ {x : G}, x self.carrier-x self.carrier

                              G is closed under negation

                            Instances For
                              theorem AddSubgroup.instSetLikeAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] (p : AddSubgroup G) (q : AddSubgroup G) (h : (fun (s : AddSubgroup G) => s.carrier) p = (fun (s : AddSubgroup G) => s.carrier) q) :
                              p = q
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Equations
                              • One or more equations did not get rendered due to their size.
                              @[simp]
                              theorem AddSubgroup.mem_carrier {G : Type u_1} [AddGroup G] {s : AddSubgroup G} {x : G} :
                              x s.carrier x s
                              @[simp]
                              theorem Subgroup.mem_carrier {G : Type u_1} [Group G] {s : Subgroup G} {x : G} :
                              x s.carrier x s
                              @[simp]
                              theorem AddSubgroup.mem_mk {G : Type u_1} [AddGroup G] {s : Set G} {x : G} (h_one : ∀ {a b : G}, a 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} [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} [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} [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} [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} [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} [AddGroup G] (K : AddSubgroup G) :
                              K.toAddSubmonoid = K
                              @[simp]
                              theorem Subgroup.coe_toSubmonoid {G : Type u_1} [Group G] (K : Subgroup G) :
                              K.toSubmonoid = K
                              @[simp]
                              theorem AddSubgroup.mem_toAddSubmonoid {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (x : G) :
                              x K.toAddSubmonoid x K
                              @[simp]
                              theorem Subgroup.mem_toSubmonoid {G : Type u_1} [Group G] (K : Subgroup G) (x : G) :
                              x K.toSubmonoid x K
                              theorem AddSubgroup.toAddSubmonoid_injective {G : Type u_1} [AddGroup G] :
                              Function.Injective AddSubgroup.toAddSubmonoid
                              theorem Subgroup.toSubmonoid_injective {G : Type u_1} [Group G] :
                              Function.Injective Subgroup.toSubmonoid
                              @[simp]
                              theorem AddSubgroup.toAddSubmonoid_eq {G : Type u_1} [AddGroup G] {p : AddSubgroup G} {q : AddSubgroup G} :
                              p.toAddSubmonoid = q.toAddSubmonoid p = q
                              @[simp]
                              theorem Subgroup.toSubmonoid_eq {G : Type u_1} [Group G] {p : Subgroup G} {q : Subgroup G} :
                              p.toSubmonoid = q.toSubmonoid p = q
                              theorem AddSubgroup.toAddSubmonoid_strictMono {G : Type u_1} [AddGroup G] :
                              StrictMono AddSubgroup.toAddSubmonoid
                              theorem Subgroup.toSubmonoid_strictMono {G : Type u_1} [Group G] :
                              StrictMono Subgroup.toSubmonoid
                              theorem AddSubgroup.toAddSubmonoid_mono {G : Type u_1} [AddGroup G] :
                              Monotone AddSubgroup.toAddSubmonoid
                              theorem Subgroup.toSubmonoid_mono {G : Type u_1} [Group G] :
                              Monotone Subgroup.toSubmonoid
                              @[simp]
                              theorem AddSubgroup.toAddSubmonoid_le {G : Type u_1} [AddGroup G] {p : AddSubgroup G} {q : AddSubgroup G} :
                              p.toAddSubmonoid q.toAddSubmonoid p q
                              @[simp]
                              theorem Subgroup.toSubmonoid_le {G : Type u_1} [Group G] {p : Subgroup G} {q : Subgroup G} :
                              p.toSubmonoid q.toSubmonoid p q
                              @[simp]
                              theorem AddSubgroup.coe_nonempty {G : Type u_1} [AddGroup G] (s : AddSubgroup G) :
                              @[simp]
                              theorem Subgroup.coe_nonempty {G : Type u_1} [Group G] (s : Subgroup G) :

                              Conversion to/from Additive/Multiplicative #

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

                              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.
                              Instances For
                                @[inline, reducible]

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

                                Equations
                                Instances For
                                  @[simp]
                                  theorem AddSubgroup.toSubgroup_apply_coe {A : Type u_4} [AddGroup A] (S : AddSubgroup A) :
                                  (AddSubgroup.toSubgroup S) = Multiplicative.toAdd ⁻¹' S
                                  @[simp]
                                  theorem AddSubgroup.toSubgroup_symm_apply_coe {A : Type u_4} [AddGroup A] (S : Subgroup (Multiplicative A)) :
                                  ((RelIso.symm AddSubgroup.toSubgroup) S) = Additive.toMul ⁻¹' S

                                  Additive subgroups 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.
                                  Instances For
                                    @[inline, reducible]

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

                                    Equations
                                    Instances For
                                      theorem AddSubgroup.copy.proof_2 {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :
                                      0 { carrier := s, add_mem' := (_ : ∀ {a b : G}, a sb sa + b s) }.carrier
                                      theorem AddSubgroup.copy.proof_3 {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :
                                      ∀ {x : G}, x { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : G}, a 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
                                      theorem AddSubgroup.copy.proof_1 {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :
                                      ∀ {a b : G}, a sb sa + b s
                                      def AddSubgroup.copy {G : Type u_1} [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.
                                      Instances For
                                        def Subgroup.copy {G : Type u_1} [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.
                                        Instances For
                                          @[simp]
                                          theorem AddSubgroup.coe_copy {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :
                                          (AddSubgroup.copy K s hs) = s
                                          @[simp]
                                          theorem Subgroup.coe_copy {G : Type u_1} [Group G] (K : Subgroup G) (s : Set G) (hs : s = K) :
                                          (Subgroup.copy K s hs) = s
                                          theorem AddSubgroup.copy_eq {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :
                                          theorem Subgroup.copy_eq {G : Type u_1} [Group G] (K : Subgroup G) (s : Set G) (hs : s = K) :
                                          Subgroup.copy K s hs = K
                                          theorem AddSubgroup.ext {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : ∀ (x : G), x H x K) :
                                          H = K

                                          Two AddSubgroups are equal if they have the same elements.

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

                                          Two subgroups are equal if they have the same elements.

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

                                          An AddSubgroup contains the group's 0.

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

                                          A subgroup contains the group's 1.

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

                                          An AddSubgroup is closed under addition.

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

                                          A subgroup is closed under multiplication.

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

                                          An AddSubgroup is closed under inverse.

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

                                          A subgroup is closed under inverse.

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

                                          An AddSubgroup is closed under subtraction.

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

                                          A subgroup is closed under division.

                                          theorem AddSubgroup.neg_mem_iff {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x : G} :
                                          -x H x H
                                          theorem Subgroup.inv_mem_iff {G : Type u_1} [Group G] (H : Subgroup G) {x : G} :
                                          x⁻¹ H x H
                                          theorem AddSubgroup.sub_mem_comm_iff {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {a : G} {b : G} :
                                          a - b H b - a H
                                          theorem Subgroup.div_mem_comm_iff {G : Type u_1} [Group G] (H : Subgroup G) {a : G} {b : G} :
                                          a / b H b / a H
                                          theorem AddSubgroup.exists_neg_mem_iff_exists_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {P : GProp} :
                                          (∃ x ∈ K, P (-x)) ∃ x ∈ K, P x
                                          theorem Subgroup.exists_inv_mem_iff_exists_mem {G : Type u_1} [Group G] (K : Subgroup G) {P : GProp} :
                                          (∃ x ∈ K, P x⁻¹) ∃ x ∈ K, P x
                                          theorem AddSubgroup.add_mem_cancel_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x : G} {y : G} (h : x H) :
                                          y + x H y H
                                          theorem Subgroup.mul_mem_cancel_right {G : Type u_1} [Group G] (H : Subgroup G) {x : G} {y : G} (h : x H) :
                                          y * x H y H
                                          theorem AddSubgroup.add_mem_cancel_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x : G} {y : G} (h : x H) :
                                          x + y H y H
                                          theorem Subgroup.mul_mem_cancel_left {G : Type u_1} [Group G] (H : Subgroup G) {x : G} {y : G} (h : x H) :
                                          x * y H y H
                                          theorem AddSubgroup.nsmul_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {x : G} (hx : x K) (n : ) :
                                          n x K
                                          theorem Subgroup.pow_mem {G : Type u_1} [Group G] (K : Subgroup G) {x : G} (hx : x K) (n : ) :
                                          x ^ n K
                                          theorem AddSubgroup.zsmul_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {x : G} (hx : x K) (n : ) :
                                          n x K
                                          theorem Subgroup.zpow_mem {G : Type u_1} [Group G] (K : Subgroup G) {x : G} (hx : x K) (n : ) :
                                          x ^ n K
                                          def AddSubgroup.ofSub {G : Type u_1} [AddGroup G] (s : Set G) (hsn : Set.Nonempty s) (hs : xs, ys, x + -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.
                                          Instances For
                                            theorem AddSubgroup.ofSub.proof_2 {G : Type u_1} [AddGroup G] (s : Set G) (hs : xs, ys, x + -y s) (one_mem : 0 s) (x : G) (hx : x s) :
                                            -x s
                                            theorem AddSubgroup.ofSub.proof_3 {G : Type u_1} [AddGroup G] (s : Set G) (hs : xs, ys, x + -y s) (inv_mem : xs, -x s) :
                                            ∀ {a b : G}, a sb sa + b s
                                            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 : G), x s))motive hsn
                                            Equations
                                            • (_ : motive hsn) = (_ : motive hsn)
                                            Instances For
                                              theorem AddSubgroup.ofSub.proof_1 {G : Type u_1} [AddGroup G] (s : Set G) (hsn : Set.Nonempty s) (hs : xs, ys, x + -y s) :
                                              0 s
                                              def Subgroup.ofDiv {G : Type u_1} [Group G] (s : Set G) (hsn : Set.Nonempty s) (hs : xs, ys, x * 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.
                                              Instances For
                                                instance AddSubgroup.add {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                Add H

                                                An AddSubgroup of an AddGroup inherits an addition.

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

                                                A subgroup of a group inherits a multiplication.

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

                                                An AddSubgroup of an AddGroup inherits a zero.

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

                                                A subgroup of a group inherits a 1.

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

                                                An AddSubgroup of an AddGroup inherits an inverse.

                                                Equations
                                                theorem AddSubgroup.neg.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (a : H) :
                                                -a H
                                                instance Subgroup.inv {G : Type u_1} [Group G] (H : Subgroup G) :
                                                Inv H

                                                A subgroup of a group inherits an inverse.

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

                                                An AddSubgroup of an AddGroup inherits a subtraction.

                                                Equations
                                                • AddSubgroup.sub H = { sub := fun (a b : H) => { val := a - b, property := (_ : a - b H) } }
                                                theorem AddSubgroup.sub.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (a : H) (b : H) :
                                                a - b H
                                                instance Subgroup.div {G : Type u_1} [Group G] (H : Subgroup G) :
                                                Div H

                                                A subgroup of a group inherits a division

                                                Equations
                                                • Subgroup.div H = { div := fun (a b : H) => { val := a / b, property := (_ : a / b H) } }
                                                instance AddSubgroup.nsmul {G : Type u_5} [AddGroup G] {H : AddSubgroup G} :
                                                SMul H

                                                An AddSubgroup of an AddGroup inherits a natural scaling.

                                                Equations
                                                • AddSubgroup.nsmul = { smul := fun (n : ) (a : H) => { val := n a, property := (_ : n a H) } }
                                                instance Subgroup.npow {G : Type u_1} [Group G] (H : Subgroup G) :
                                                Pow H

                                                A subgroup of a group inherits a natural power

                                                Equations
                                                • Subgroup.npow H = { pow := fun (a : H) (n : ) => { val := a ^ n, property := (_ : a ^ n H) } }
                                                instance AddSubgroup.zsmul {G : Type u_5} [AddGroup G] {H : AddSubgroup G} :
                                                SMul H

                                                An AddSubgroup of an AddGroup inherits an integer scaling.

                                                Equations
                                                • AddSubgroup.zsmul = { smul := fun (n : ) (a : H) => { val := n a, property := (_ : n a H) } }
                                                instance Subgroup.zpow {G : Type u_1} [Group G] (H : Subgroup G) :
                                                Pow H

                                                A subgroup of a group inherits an integer power

                                                Equations
                                                • Subgroup.zpow H = { pow := fun (a : H) (n : ) => { val := a ^ n, property := (_ : a ^ n H) } }
                                                @[simp]
                                                theorem AddSubgroup.coe_add {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : H) (y : H) :
                                                (x + y) = x + y
                                                @[simp]
                                                theorem Subgroup.coe_mul {G : Type u_1} [Group G] (H : Subgroup G) (x : H) (y : H) :
                                                (x * y) = x * y
                                                @[simp]
                                                theorem AddSubgroup.coe_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                0 = 0
                                                @[simp]
                                                theorem Subgroup.coe_one {G : Type u_1} [Group G] (H : Subgroup G) :
                                                1 = 1
                                                @[simp]
                                                theorem AddSubgroup.coe_neg {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : H) :
                                                (-x) = -x
                                                @[simp]
                                                theorem Subgroup.coe_inv {G : Type u_1} [Group G] (H : Subgroup G) (x : H) :
                                                x⁻¹ = (x)⁻¹
                                                @[simp]
                                                theorem AddSubgroup.coe_sub {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : H) (y : H) :
                                                (x - y) = x - y
                                                @[simp]
                                                theorem Subgroup.coe_div {G : Type u_1} [Group G] (H : Subgroup G) (x : H) (y : H) :
                                                (x / y) = x / y
                                                theorem AddSubgroup.coe_mk {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : G) (hx : x H) :
                                                { val := x, property := hx } = x
                                                theorem Subgroup.coe_mk {G : Type u_1} [Group G] (H : Subgroup G) (x : G) (hx : x H) :
                                                { val := x, property := hx } = x
                                                @[simp]
                                                theorem AddSubgroup.coe_nsmul {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : H) (n : ) :
                                                (n x) = n x
                                                @[simp]
                                                theorem Subgroup.coe_pow {G : Type u_1} [Group G] (H : Subgroup G) (x : H) (n : ) :
                                                (x ^ n) = x ^ n
                                                theorem AddSubgroup.coe_zsmul {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : H) (n : ) :
                                                (n x) = n x
                                                theorem Subgroup.coe_zpow {G : Type u_1} [Group G] (H : Subgroup G) (x : H) (n : ) :
                                                (x ^ n) = x ^ n
                                                @[simp]
                                                theorem AddSubgroup.mk_eq_zero_iff {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {g : G} {h : g H} :
                                                { val := g, property := h } = 0 g = 0
                                                @[simp]
                                                theorem Subgroup.mk_eq_one_iff {G : Type u_1} [Group G] (H : Subgroup G) {g : G} {h : g H} :
                                                { val := g, property := h } = 1 g = 1
                                                theorem AddSubgroup.toAddGroup.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                Function.Injective fun (a : H) => a
                                                theorem AddSubgroup.toAddGroup.proof_6 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                ∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
                                                instance AddSubgroup.toAddGroup {G : Type u_5} [AddGroup G] (H : AddSubgroup G) :

                                                An AddSubgroup of an AddGroup inherits an AddGroup structure.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                theorem AddSubgroup.toAddGroup.proof_4 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                ∀ (x : H), (-x) = (-x)
                                                theorem AddSubgroup.toAddGroup.proof_7 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                ∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
                                                theorem AddSubgroup.toAddGroup.proof_3 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                ∀ (x x_1 : H), (x + x_1) = (x + x_1)
                                                theorem AddSubgroup.toAddGroup.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                0 = 0
                                                theorem AddSubgroup.toAddGroup.proof_5 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                ∀ (x x_1 : H), (x - x_1) = (x - x_1)
                                                instance Subgroup.toGroup {G : Type u_5} [Group G] (H : Subgroup G) :
                                                Group H

                                                A subgroup of a group inherits a group structure.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                theorem AddSubgroup.toAddCommGroup.proof_4 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) :
                                                ∀ (x : H), (-x) = (-x)

                                                An AddSubgroup of an AddCommGroup is an AddCommGroup.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                theorem AddSubgroup.toAddCommGroup.proof_6 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) :
                                                ∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
                                                theorem AddSubgroup.toAddCommGroup.proof_7 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) :
                                                ∀ (x : H) (x_1 : ), (x_1 x) = (x_1 x)
                                                theorem AddSubgroup.toAddCommGroup.proof_1 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) :
                                                Function.Injective fun (a : H) => a
                                                theorem AddSubgroup.toAddCommGroup.proof_3 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) :
                                                ∀ (x x_1 : H), (x + x_1) = (x + x_1)
                                                theorem AddSubgroup.toAddCommGroup.proof_5 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) :
                                                ∀ (x x_1 : H), (x - x_1) = (x - x_1)
                                                instance Subgroup.toCommGroup {G : Type u_5} [CommGroup G] (H : Subgroup G) :

                                                A subgroup of a CommGroup is a CommGroup.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                def AddSubgroup.subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                H →+ G

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

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  theorem AddSubgroup.subtype.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                  0 = 0
                                                  theorem AddSubgroup.subtype.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                  ∀ (x x_1 : H), { toFun := Subtype.val, map_zero' := (_ : 0 = 0) }.toFun (x + x_1) = { toFun := Subtype.val, map_zero' := (_ : 0 = 0) }.toFun (x + x_1)
                                                  def Subgroup.subtype {G : Type u_1} [Group G] (H : Subgroup G) :
                                                  H →* G

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

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem AddSubgroup.coeSubtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                    (AddSubgroup.subtype H) = Subtype.val
                                                    @[simp]
                                                    theorem Subgroup.coeSubtype {G : Type u_1} [Group G] (H : Subgroup G) :
                                                    (Subgroup.subtype H) = Subtype.val
                                                    theorem AddSubgroup.inclusion.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) (x : H) :
                                                    x K
                                                    def AddSubgroup.inclusion {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) :
                                                    H →+ K

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

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      theorem AddSubgroup.inclusion.proof_2 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) :
                                                      ∀ (x x_1 : H), (fun (x : H) => { val := x, property := (_ : x K) }) (x + x_1) = (fun (x : H) => { val := x, property := (_ : x K) }) (x + x_1)
                                                      def Subgroup.inclusion {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H K) :
                                                      H →* K

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

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        theorem AddSubgroup.coe_inclusion {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {h : H K} (a : H) :
                                                        ((AddSubgroup.inclusion h) a) = a
                                                        @[simp]
                                                        theorem Subgroup.coe_inclusion {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {h : H K} (a : H) :
                                                        ((Subgroup.inclusion h) a) = a
                                                        theorem AddSubgroup.instTopAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] :
                                                        ∀ {x : G}, x .carrier-x Set.univ

                                                        The AddSubgroup G of the AddGroup G.

                                                        Equations
                                                        • AddSubgroup.instTopAddSubgroup = { top := let src := ; { toAddSubmonoid := src, neg_mem' := (_ : ∀ {x : G}, x .carrier-x Set.univ) } }
                                                        instance Subgroup.instTopSubgroup {G : Type u_1} [Group G] :

                                                        The subgroup G of the group G.

                                                        Equations
                                                        • Subgroup.instTopSubgroup = { top := let src := ; { toSubmonoid := src, inv_mem' := (_ : ∀ {x : G}, x .carrierx⁻¹ Set.univ) } }
                                                        def AddSubgroup.topEquiv {G : Type u_1} [AddGroup G] :
                                                        ≃+ 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
                                                        Instances For
                                                          @[simp]
                                                          theorem Subgroup.topEquiv_apply {G : Type u_1} [Group G] (x : ) :
                                                          Subgroup.topEquiv x = x
                                                          @[simp]
                                                          theorem AddSubgroup.topEquiv_symm_apply_coe {G : Type u_1} [AddGroup G] (x : G) :
                                                          ((AddEquiv.symm AddSubgroup.topEquiv) x) = x
                                                          @[simp]
                                                          theorem AddSubgroup.topEquiv_apply {G : Type u_1} [AddGroup G] (x : ) :
                                                          AddSubgroup.topEquiv x = x
                                                          @[simp]
                                                          theorem Subgroup.topEquiv_symm_apply_coe {G : Type u_1} [Group G] (x : G) :
                                                          ((MulEquiv.symm Subgroup.topEquiv) x) = x
                                                          def Subgroup.topEquiv {G : Type u_1} [Group G] :
                                                          ≃* G

                                                          The top subgroup is isomorphic to the group.

                                                          This is the group version of Submonoid.topEquiv.

                                                          Equations
                                                          • Subgroup.topEquiv = Submonoid.topEquiv
                                                          Instances For

                                                            The trivial AddSubgroup {0} of an AddGroup G.

                                                            Equations
                                                            • AddSubgroup.instBotAddSubgroup = { bot := let src := ; { toAddSubmonoid := src, neg_mem' := (_ : a.carrier, -a .carrier) } }
                                                            theorem AddSubgroup.instBotAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] (a : G) :
                                                            a .carrier-a .carrier
                                                            instance Subgroup.instBotSubgroup {G : Type u_1} [Group G] :

                                                            The trivial subgroup {1} of a group G.

                                                            Equations
                                                            • Subgroup.instBotSubgroup = { bot := let src := ; { toSubmonoid := src, inv_mem' := (_ : a.carrier, a⁻¹ .carrier) } }
                                                            Equations
                                                            • AddSubgroup.instInhabitedAddSubgroup = { default := }
                                                            Equations
                                                            • Subgroup.instInhabitedSubgroup = { default := }
                                                            @[simp]
                                                            theorem AddSubgroup.mem_bot {G : Type u_1} [AddGroup G] {x : G} :
                                                            x x = 0
                                                            @[simp]
                                                            theorem Subgroup.mem_bot {G : Type u_1} [Group G] {x : G} :
                                                            x x = 1
                                                            @[simp]
                                                            theorem AddSubgroup.mem_top {G : Type u_1} [AddGroup G] (x : G) :
                                                            @[simp]
                                                            theorem Subgroup.mem_top {G : Type u_1} [Group G] (x : G) :
                                                            @[simp]
                                                            theorem AddSubgroup.coe_top {G : Type u_1} [AddGroup G] :
                                                            = Set.univ
                                                            @[simp]
                                                            theorem Subgroup.coe_top {G : Type u_1} [Group G] :
                                                            = Set.univ
                                                            @[simp]
                                                            theorem AddSubgroup.coe_bot {G : Type u_1} [AddGroup G] :
                                                            = {0}
                                                            @[simp]
                                                            theorem Subgroup.coe_bot {G : Type u_1} [Group G] :
                                                            = {1}
                                                            Equations
                                                            • AddSubgroup.instUniqueSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroupBotInstBotAddSubgroup = { toInhabited := { default := 0 }, uniq := (_ : ∀ (g : ), g = default) }
                                                            Equations
                                                            • Subgroup.instUniqueSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupBotInstBotSubgroup = { toInhabited := { default := 1 }, uniq := (_ : ∀ (g : ), g = default) }
                                                            @[simp]
                                                            theorem AddSubgroup.top_toAddSubmonoid {G : Type u_1} [AddGroup G] :
                                                            .toAddSubmonoid =
                                                            @[simp]
                                                            theorem Subgroup.top_toSubmonoid {G : Type u_1} [Group G] :
                                                            .toSubmonoid =
                                                            @[simp]
                                                            theorem AddSubgroup.bot_toAddSubmonoid {G : Type u_1} [AddGroup G] :
                                                            .toAddSubmonoid =
                                                            @[simp]
                                                            theorem Subgroup.bot_toSubmonoid {G : Type u_1} [Group G] :
                                                            .toSubmonoid =
                                                            theorem AddSubgroup.eq_bot_iff_forall {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                            H = xH, x = 0
                                                            theorem Subgroup.eq_bot_iff_forall {G : Type u_1} [Group G] (H : Subgroup G) :
                                                            H = xH, x = 1
                                                            @[simp]
                                                            theorem AddSubgroup.coe_eq_univ {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                            H = Set.univ H =
                                                            @[simp]
                                                            theorem Subgroup.coe_eq_univ {G : Type u_1} [Group G] {H : Subgroup G} :
                                                            H = Set.univ H =
                                                            theorem AddSubgroup.coe_eq_singleton {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                            (∃ (g : G), H = {g}) H =
                                                            abbrev AddSubgroup.coe_eq_singleton.match_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (motive : (∃ (g : G), H = {g})Prop) :
                                                            ∀ (x : ∃ (g : G), H = {g}), (∀ (g : G) (hg : H = {g}), motive (_ : ∃ (g : G), H = {g}))motive x
                                                            Equations
                                                            • (_ : motive x) = (_ : motive x)
                                                            Instances For
                                                              theorem Subgroup.coe_eq_singleton {G : Type u_1} [Group G] {H : Subgroup G} :
                                                              (∃ (g : G), H = {g}) H =
                                                              theorem AddSubgroup.nontrivial_iff_exists_ne_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                              Nontrivial H ∃ x ∈ H, x 0
                                                              theorem Subgroup.nontrivial_iff_exists_ne_one {G : Type u_1} [Group G] (H : Subgroup G) :
                                                              Nontrivial H ∃ x ∈ H, x 1
                                                              theorem AddSubgroup.exists_ne_zero_of_nontrivial {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Nontrivial H] :
                                                              ∃ x ∈ H, x 0
                                                              theorem Subgroup.exists_ne_one_of_nontrivial {G : Type u_1} [Group G] (H : Subgroup G) [Nontrivial H] :
                                                              ∃ x ∈ H, x 1

                                                              A subgroup is either the trivial subgroup or nontrivial.

                                                              theorem Subgroup.bot_or_nontrivial {G : Type u_1} [Group G] (H : Subgroup G) :

                                                              A subgroup is either the trivial subgroup or nontrivial.

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

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

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

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

                                                              theorem AddSubgroup.ne_bot_iff_exists_ne_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                              H ∃ (a : H), a 0
                                                              theorem Subgroup.ne_bot_iff_exists_ne_one {G : Type u_1} [Group G] {H : Subgroup G} :
                                                              H ∃ (a : H), a 1

                                                              The inf of two AddSubgroups is their intersection.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              theorem AddSubgroup.instInfAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] (H₁ : AddSubgroup G) (H₂ : AddSubgroup G) :
                                                              ∀ {x : G}, x (H₁.toAddSubmonoid H₂.toAddSubmonoid).carrier-x (H₁.toAddSubmonoid H₂.toAddSubmonoid).carrier
                                                              abbrev AddSubgroup.instInfAddSubgroup.match_1 {G : Type u_1} [AddGroup G] (H₁ : AddSubgroup G) (H₂ : AddSubgroup G) :
                                                              ∀ {x : G}, let src := H₁.toAddSubmonoid H₂.toAddSubmonoid; ∀ (motive : x src.carrierProp) (x_1 : x src.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.
                                                              Instances For
                                                                instance Subgroup.instInfSubgroup {G : Type u_1} [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} [AddGroup G] (p : AddSubgroup G) (p' : AddSubgroup G) :
                                                                (p p') = p p'
                                                                @[simp]
                                                                theorem Subgroup.coe_inf {G : Type u_1} [Group G] (p : Subgroup G) (p' : Subgroup G) :
                                                                (p p') = p p'
                                                                @[simp]
                                                                theorem AddSubgroup.mem_inf {G : Type u_1} [AddGroup G] {p : AddSubgroup G} {p' : AddSubgroup G} {x : G} :
                                                                x p p' x p x p'
                                                                @[simp]
                                                                theorem Subgroup.mem_inf {G : Type u_1} [Group G] {p : Subgroup G} {p' : Subgroup G} {x : G} :
                                                                x p p' x p x p'
                                                                theorem AddSubgroup.instInfSetAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) :
                                                                ⋂ S ∈ s, S = (⨅ i ∈ s, i.toAddSubmonoid)
                                                                theorem AddSubgroup.instInfSetAddSubgroup.proof_2 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) {x : G} (hx : x (AddSubmonoid.copy (⨅ S ∈ s, S.toAddSubmonoid) (⋂ S ∈ s, S) (_ : ⋂ S ∈ s, S = (⨅ i ∈ s, i.toAddSubmonoid))).toAddSubsemigroup.carrier) :
                                                                -x ⋂ x ∈ s, x
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                @[simp]
                                                                theorem AddSubgroup.coe_sInf {G : Type u_1} [AddGroup G] (H : Set (AddSubgroup G)) :
                                                                (sInf H) = ⋂ s ∈ H, s
                                                                @[simp]
                                                                theorem Subgroup.coe_sInf {G : Type u_1} [Group G] (H : Set (Subgroup G)) :
                                                                (sInf H) = ⋂ s ∈ H, s
                                                                @[simp]
                                                                theorem AddSubgroup.mem_sInf {G : Type u_1} [AddGroup G] {S : Set (AddSubgroup G)} {x : G} :
                                                                x sInf S pS, x p
                                                                @[simp]
                                                                theorem Subgroup.mem_sInf {G : Type u_1} [Group G] {S : Set (Subgroup G)} {x : G} :
                                                                x sInf S pS, x p
                                                                theorem AddSubgroup.mem_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_5} {S : ιAddSubgroup G} {x : G} :
                                                                x ⨅ (i : ι), S i ∀ (i : ι), x S i
                                                                theorem Subgroup.mem_iInf {G : Type u_1} [Group G] {ι : Sort u_5} {S : ιSubgroup G} {x : G} :
                                                                x ⨅ (i : ι), S i ∀ (i : ι), x S i
                                                                @[simp]
                                                                theorem AddSubgroup.coe_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_5} {S : ιAddSubgroup G} :
                                                                (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
                                                                @[simp]
                                                                theorem Subgroup.coe_iInf {G : Type u_1} [Group G] {ι : Sort u_5} {S : ιSubgroup G} :
                                                                (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
                                                                theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_3 {G : Type u_1} [AddGroup G] (_a : AddSubgroup G) (_b : AddSubgroup G) (_x : G) (self : _x _a.toAddSubmonoid _x _b.toAddSubmonoid) :
                                                                _x _b.toAddSubmonoid

                                                                The AddSubgroups of an AddGroup form a complete lattice.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_6 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) :
                                                                (bs, b a)sSup s a
                                                                theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_9 {G : Type u_1} [AddGroup G] (S : AddSubgroup G) (_x : G) (hx : _x ) :
                                                                _x S
                                                                theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_2 {G : Type u_1} [AddGroup G] (_a : AddSubgroup G) (_b : AddSubgroup G) (_x : G) (self : _x _a.toAddSubmonoid _x _b.toAddSubmonoid) :
                                                                _x _a.toAddSubmonoid
                                                                theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_8 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) :
                                                                (bs, a b)a sInf s
                                                                theorem AddSubgroup.instCompleteLatticeAddSubgroup.proof_4 {G : Type u_1} [AddGroup G] (_a : AddSubgroup G) (_b : AddSubgroup G) (_c : AddSubgroup G) (ha : _a _b) (hb : _a _c) (_x : G) (hx : _x _a) :
                                                                _x _b.toAddSubmonoid _x _c.toAddSubmonoid

                                                                Subgroups of a group form a complete lattice.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                theorem AddSubgroup.mem_sup_left {G : Type u_1} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} {x : G} :
                                                                x Sx S T
                                                                theorem Subgroup.mem_sup_left {G : Type u_1} [Group G] {S : Subgroup G} {T : Subgroup G} {x : G} :
                                                                x Sx S T
                                                                theorem AddSubgroup.mem_sup_right {G : Type u_1} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} {x : G} :
                                                                x Tx S T
                                                                theorem Subgroup.mem_sup_right {G : Type u_1} [Group G] {S : Subgroup G} {T : Subgroup G} {x : G} :
                                                                x Tx S T
                                                                theorem AddSubgroup.add_mem_sup {G : Type u_1} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} {x : G} {y : G} (hx : x S) (hy : y T) :
                                                                x + y S T
                                                                theorem Subgroup.mul_mem_sup {G : Type u_1} [Group G] {S : Subgroup G} {T : Subgroup G} {x : G} {y : G} (hx : x S) (hy : y T) :
                                                                x * y S T
                                                                theorem AddSubgroup.mem_iSup_of_mem {G : Type u_1} [AddGroup G] {ι : Sort u_5} {S : ιAddSubgroup G} (i : ι) {x : G} :
                                                                x S ix iSup S
                                                                theorem Subgroup.mem_iSup_of_mem {G : Type u_1} [Group G] {ι : Sort u_5} {S : ιSubgroup G} (i : ι) {x : G} :
                                                                x S ix iSup S
                                                                theorem AddSubgroup.mem_sSup_of_mem {G : Type u_1} [AddGroup G] {S : Set (AddSubgroup G)} {s : AddSubgroup G} (hs : s S) {x : G} :
                                                                x sx sSup S
                                                                theorem Subgroup.mem_sSup_of_mem {G : Type u_1} [Group G] {S : Set (Subgroup G)} {s : Subgroup G} (hs : s S) {x : G} :
                                                                x sx sSup S
                                                                Equations
                                                                • AddSubgroup.instUniqueAddSubgroup = { toInhabited := { default := }, uniq := (_ : ∀ (a : AddSubgroup G), a = default) }
                                                                Equations
                                                                • Subgroup.instUniqueSubgroup = { toInhabited := { default := }, uniq := (_ : ∀ (a : Subgroup G), a = default) }
                                                                theorem AddSubgroup.eq_top_iff' {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                                H = ∀ (x : G), x H
                                                                theorem Subgroup.eq_top_iff' {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                H = ∀ (x : G), x H
                                                                def AddSubgroup.closure {G : Type u_1} [AddGroup G] (k : Set G) :

                                                                The AddSubgroup generated by a set

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

                                                                  The Subgroup generated by a set.

                                                                  Equations
                                                                  Instances For
                                                                    theorem AddSubgroup.mem_closure {G : Type u_1} [AddGroup G] {k : Set G} {x : G} :
                                                                    x AddSubgroup.closure k ∀ (K : AddSubgroup G), k Kx K
                                                                    theorem Subgroup.mem_closure {G : Type u_1} [Group G] {k : Set G} {x : G} :
                                                                    x Subgroup.closure k ∀ (K : Subgroup G), k Kx K
                                                                    @[simp]
                                                                    theorem AddSubgroup.subset_closure {G : Type u_1} [AddGroup G] {k : Set G} :

                                                                    The AddSubgroup generated by a set includes the set.

                                                                    @[simp]
                                                                    theorem Subgroup.subset_closure {G : Type u_1} [Group G] {k : Set G} :

                                                                    The subgroup generated by a set includes the set.

                                                                    theorem AddSubgroup.not_mem_of_not_mem_closure {G : Type u_1} [AddGroup G] {k : Set G} {P : G} (hP : PAddSubgroup.closure k) :
                                                                    Pk
                                                                    theorem Subgroup.not_mem_of_not_mem_closure {G : Type u_1} [Group G] {k : Set G} {P : G} (hP : PSubgroup.closure k) :
                                                                    Pk
                                                                    @[simp]
                                                                    theorem AddSubgroup.closure_le {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {k : Set G} :

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

                                                                    @[simp]
                                                                    theorem Subgroup.closure_le {G : Type u_1} [Group G] (K : Subgroup G) {k : Set G} :

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

                                                                    theorem AddSubgroup.closure_eq_of_le {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {k : Set G} (h₁ : k K) (h₂ : K AddSubgroup.closure k) :
                                                                    theorem Subgroup.closure_eq_of_le {G : Type u_1} [Group G] (K : Subgroup G) {k : Set G} (h₁ : k K) (h₂ : K Subgroup.closure k) :
                                                                    theorem AddSubgroup.closure_induction {G : Type u_1} [AddGroup G] {k : Set G} {p : GProp} {x : G} (h : x AddSubgroup.closure k) (Hk : xk, p x) (H1 : p 0) (Hmul : ∀ (x y : G), p xp yp (x + y)) (Hinv : ∀ (x : G), p xp (-x)) :
                                                                    p x

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

                                                                    theorem Subgroup.closure_induction {G : Type u_1} [Group G] {k : Set G} {p : GProp} {x : G} (h : x Subgroup.closure k) (Hk : xk, p x) (H1 : p 1) (Hmul : ∀ (x y : G), p xp yp (x * y)) (Hinv : ∀ (x : G), p xp x⁻¹) :
                                                                    p x

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

                                                                    abbrev AddSubgroup.closure_induction'.match_1 {G : Type u_1} [AddGroup G] {k : Set G} {p : (x : G) → x AddSubgroup.closure kProp} (y : G) (motive : (∃ (x : y AddSubgroup.closure k), p y x)Prop) :
                                                                    ∀ (x : ∃ (x : y AddSubgroup.closure k), p y x), (∀ (hy' : y AddSubgroup.closure k) (hy : p y hy'), motive (_ : ∃ (x : y AddSubgroup.closure k), p y x))motive x
                                                                    Equations
                                                                    • (_ : motive x) = (_ : motive x)
                                                                    Instances For
                                                                      theorem AddSubgroup.closure_induction' {G : Type u_1} [AddGroup G] {k : Set G} {p : (x : G) → x AddSubgroup.closure kProp} (Hs : ∀ (x : G) (h : x k), p x (_ : x (AddSubgroup.closure k))) (H1 : p 0 (_ : 0 AddSubgroup.closure k)) (Hmul : ∀ (x : G) (hx : x AddSubgroup.closure k) (y : G) (hy : y AddSubgroup.closure k), p x hxp y hyp (x + y) (_ : x + y AddSubgroup.closure k)) (Hinv : ∀ (x : G) (hx : x AddSubgroup.closure k), p x hxp (-x) (_ : -x AddSubgroup.closure k)) {x : G} (hx : x AddSubgroup.closure k) :
                                                                      p x hx

                                                                      A dependent version of AddSubgroup.closure_induction.

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

                                                                      A dependent version of Subgroup.closure_induction.

                                                                      theorem AddSubgroup.closure_induction₂ {G : Type u_1} [AddGroup G] {k : Set G} {p : GGProp} {x : G} {y : G} (hx : x AddSubgroup.closure k) (hy : y AddSubgroup.closure k) (Hk : xk, yk, p x y) (H1_left : ∀ (x : G), p 0 x) (H1_right : ∀ (x : G), p x 0) (Hmul_left : ∀ (x₁ x₂ y : G), p x₁ yp x₂ yp (x₁ + x₂) y) (Hmul_right : ∀ (x y₁ y₂ : G), p x y₁p x y₂p x (y₁ + y₂)) (Hinv_left : ∀ (x y : G), p x yp (-x) y) (Hinv_right : ∀ (x y : G), p x yp x (-y)) :
                                                                      p x y

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

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

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

                                                                      @[simp]
                                                                      @[simp]
                                                                      theorem Subgroup.closure_closure_coe_preimage {G : Type u_1} [Group G] {k : Set G} :
                                                                      Subgroup.closure (Subtype.val ⁻¹' k) =
                                                                      theorem AddSubgroup.closureAddCommGroupOfComm.proof_1 {G : Type u_1} [AddGroup G] {k : Set G} (hcomm : xk, yk, x + y = y + x) (x : (AddSubgroup.closure k)) (y : (AddSubgroup.closure k)) :
                                                                      x + y = y + x
                                                                      def AddSubgroup.closureAddCommGroupOfComm {G : Type u_1} [AddGroup G] {k : Set G} (hcomm : xk, yk, x + y = y + x) :

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

                                                                      Equations
                                                                      Instances For
                                                                        def Subgroup.closureCommGroupOfComm {G : Type u_1} [Group G] {k : Set G} (hcomm : xk, yk, x * y = y * x) :

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

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

                                                                          closure forms a Galois insertion with the coercion to set.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            theorem AddSubgroup.gi.proof_1 (G : Type u_1) [AddGroup G] (_s : AddSubgroup G) :
                                                                            _s (AddSubgroup.closure _s)
                                                                            theorem AddSubgroup.gi.proof_2 (G : Type u_1) [AddGroup G] (_s : Set G) (_h : (AddSubgroup.closure _s) _s) :
                                                                            (fun (s : Set G) (x : (AddSubgroup.closure s) s) => AddSubgroup.closure s) _s _h = (fun (s : Set G) (x : (AddSubgroup.closure s) s) => AddSubgroup.closure s) _s _h
                                                                            def Subgroup.gi (G : Type u_1) [Group G] :
                                                                            GaloisInsertion Subgroup.closure SetLike.coe

                                                                            closure forms a Galois insertion with the coercion to set.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              theorem AddSubgroup.closure_mono {G : Type u_1} [AddGroup G] ⦃h : Set G ⦃k : Set G (h' : h k) :

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

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

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

                                                                              @[simp]

                                                                              Additive closure of an additive subgroup K equals K

                                                                              @[simp]
                                                                              theorem Subgroup.closure_eq {G : Type u_1} [Group G] (K : Subgroup G) :

                                                                              Closure of a subgroup K equals K.

                                                                              @[simp]
                                                                              @[simp]
                                                                              theorem Subgroup.closure_univ {G : Type u_1} [Group G] :
                                                                              theorem AddSubgroup.sup_eq_closure {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (H' : AddSubgroup G) :
                                                                              H H' = AddSubgroup.closure (H H')
                                                                              theorem Subgroup.sup_eq_closure {G : Type u_1} [Group G] (H : Subgroup G) (H' : Subgroup G) :
                                                                              H H' = Subgroup.closure (H H')
                                                                              theorem AddSubgroup.closure_iUnion {G : Type u_1} [AddGroup G] {ι : Sort u_5} (s : ιSet G) :
                                                                              AddSubgroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), AddSubgroup.closure (s i)
                                                                              theorem Subgroup.closure_iUnion {G : Type u_1} [Group G] {ι : Sort u_5} (s : ιSet G) :
                                                                              Subgroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), Subgroup.closure (s i)
                                                                              @[simp]
                                                                              @[simp]
                                                                              theorem Subgroup.closure_eq_bot_iff {G : Type u_1} [Group G] {k : Set G} :
                                                                              theorem AddSubgroup.iSup_eq_closure {G : Type u_1} [AddGroup G] {ι : Sort u_5} (p : ιAddSubgroup G) :
                                                                              ⨆ (i : ι), p i = AddSubgroup.closure (⋃ (i : ι), (p i))
                                                                              theorem Subgroup.iSup_eq_closure {G : Type u_1} [Group G] {ι : Sort u_5} (p : ιSubgroup G) :
                                                                              ⨆ (i : ι), p i = Subgroup.closure (⋃ (i : ι), (p i))
                                                                              theorem AddSubgroup.mem_closure_singleton {G : Type u_1} [AddGroup G] {x : G} {y : G} :
                                                                              y AddSubgroup.closure {x} ∃ (n : ), n x = y

                                                                              The AddSubgroup generated by an element of an AddGroup equals the set of natural number multiples of the element.

                                                                              abbrev AddSubgroup.mem_closure_singleton.match_1 {G : Type u_1} [AddGroup G] {x : G} {y : G} (motive : (∃ (n : ), n x = y)Prop) :
                                                                              ∀ (x_1 : ∃ (n : ), n x = y), (∀ (n : ) (hn : n x = y), motive (_ : ∃ (n : ), n x = y))motive x_1
                                                                              Equations
                                                                              • (_ : motive x) = (_ : motive x)
                                                                              Instances For
                                                                                theorem Subgroup.mem_closure_singleton {G : Type u_1} [Group G] {x : G} {y : G} :
                                                                                y Subgroup.closure {x} ∃ (n : ), x ^ n = y

                                                                                The subgroup generated by an element of a group equals the set of integer number powers of the element.

                                                                                abbrev AddSubgroup.mem_iSup_of_directed.match_1 {G : Type u_2} [AddGroup G] {ι : Sort u_1} {K : ιAddSubgroup G} {x : G} (motive : (∃ (i : ι), x K i)Prop) :
                                                                                ∀ (x_1 : ∃ (i : ι), x K i), (∀ (i : ι) (hi : x K i), motive (_ : ∃ (i : ι), x K i))motive x_1
                                                                                Equations
                                                                                • (_ : motive x) = (_ : motive x)
                                                                                Instances For
                                                                                  theorem AddSubgroup.mem_iSup_of_directed {G : Type u_1} [AddGroup G] {ι : Sort u_5} [hι : Nonempty ι] {K : ιAddSubgroup G} (hK : Directed (fun (x x_1 : AddSubgroup G) => x x_1) K) {x : G} :
                                                                                  x iSup K ∃ (i : ι), x K i
                                                                                  theorem Subgroup.mem_iSup_of_directed {G : Type u_1} [Group G] {ι : Sort u_5} [hι : Nonempty ι] {K : ιSubgroup G} (hK : Directed (fun (x x_1 : Subgroup G) => x x_1) K) {x : G} :
                                                                                  x iSup K ∃ (i : ι), x K i
                                                                                  theorem AddSubgroup.coe_iSup_of_directed {G : Type u_1} [AddGroup G] {ι : Sort u_5} [Nonempty ι] {S : ιAddSubgroup G} (hS : Directed (fun (x x_1 : AddSubgroup G) => x x_1) S) :
                                                                                  (⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
                                                                                  theorem Subgroup.coe_iSup_of_directed {G : Type u_1} [Group G] {ι : Sort u_5} [Nonempty ι] {S : ιSubgroup G} (hS : Directed (fun (x x_1 : Subgroup G) => x x_1) S) :
                                                                                  (⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
                                                                                  theorem AddSubgroup.mem_sSup_of_directedOn {G : Type u_1} [AddGroup G] {K : Set (AddSubgroup G)} (Kne : Set.Nonempty K) (hK : DirectedOn (fun (x x_1 : AddSubgroup G) => x x_1) K) {x : G} :
                                                                                  x sSup K ∃ s ∈ K, x s
                                                                                  theorem Subgroup.mem_sSup_of_directedOn {G : Type u_1} [Group G] {K : Set (Subgroup G)} (Kne : Set.Nonempty K) (hK : DirectedOn (fun (x x_1 : Subgroup G) => x x_1) K) {x : G} :
                                                                                  x sSup K ∃ s ∈ K, x s
                                                                                  def AddSubgroup.comap {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) :

                                                                                  The preimage of an AddSubgroup along an AddMonoid homomorphism is an AddSubgroup.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    theorem AddSubgroup.comap.proof_2 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) :
                                                                                    ∀ {a b : G}, a (AddSubmonoid.comap f H.toAddSubmonoid).toAddSubsemigroup.carrierb (AddSubmonoid.comap f H.toAddSubmonoid).toAddSubsemigroup.carriera + b (AddSubmonoid.comap f H.toAddSubmonoid).toAddSubsemigroup.carrier
                                                                                    theorem AddSubgroup.comap.proof_3 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) :
                                                                                    0 (AddSubmonoid.comap f H.toAddSubmonoid).toAddSubsemigroup.carrier
                                                                                    theorem AddSubgroup.comap.proof_4 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) {a : G} (ha : a { toAddSubsemigroup := { carrier := f ⁻¹' H, add_mem' := (_ : ∀ {a b : G}, a (AddSubmonoid.comap f H.toAddSubmonoid).toAddSubsemigroup.carrierb (AddSubmonoid.comap f H.toAddSubmonoid).toAddSubsemigroup.carriera + b (AddSubmonoid.comap f H.toAddSubmonoid).toAddSubsemigroup.carrier) }, zero_mem' := (_ : 0 (AddSubmonoid.comap f H.toAddSubmonoid).toAddSubsemigroup