Documentation

Mathlib.Algebra.Group.Subgroup.Defs

Subgroups #

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

Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.

Main definitions #

Notation used here:

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_3) (G : outParam (Type u_4)) [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_3) (G : outParam (Type u_4)) [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_3) (G : outParam (Type u_4)) [DivInvMonoid G] [SetLike S G] extends SubmonoidClass S G, InvMemClass S G :

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

      Instances
        class AddSubgroupClass (S : Type u_3) (G : outParam (Type u_4)) [SubNegMonoid G] [SetLike S G] extends AddSubmonoidClass S G, NegMemClass S G :

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

        Instances
          @[simp]
          theorem inv_mem_iff {S : Type u_3} {G : Type u_4} [InvolutiveInv G] {x✝ : SetLike S G} [InvMemClass S G] {H : S} {x : G} :
          x⁻¹ H x H
          @[simp]
          theorem neg_mem_iff {S : Type u_3} {G : Type u_4} [InvolutiveNeg G] {x✝ : SetLike S G} [NegMemClass S G] {H : S} {x : G} :
          -x H x H
          theorem div_mem {M : Type u_3} {S : Type u_4} [DivInvMonoid M] [SetLike S M] [hSM : SubgroupClass S M] {H : S} {x y : M} (hx : x H) (hy : y H) :
          x / y H

          A subgroup is closed under division.

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

          An additive subgroup is closed under subtraction.

          theorem zpow_mem {M : Type u_3} {S : Type u_4} [DivInvMonoid M] [SetLike S M] [hSM : SubgroupClass S M] {K : S} {x : M} (hx : x K) (n : ) :
          x ^ n K
          theorem zsmul_mem {M : Type u_3} {S : Type u_4} [SubNegMonoid M] [SetLike S M] [hSM : AddSubgroupClass S M] {K : S} {x : M} (hx : x K) (n : ) :
          n x K
          theorem exists_inv_mem_iff_exists_mem {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] {P : GProp} :
          (∃ xH, P x⁻¹) xH, P x
          theorem exists_neg_mem_iff_exists_mem {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] {P : GProp} :
          (∃ xH, P (-x)) xH, P x
          theorem mul_mem_cancel_right {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] {x y : G} (h : x H) :
          y * x H y H
          theorem add_mem_cancel_right {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] {x y : G} (h : x H) :
          y + x H y H
          theorem mul_mem_cancel_left {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] {x y : G} (h : x H) :
          x * y H y H
          theorem add_mem_cancel_left {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] {x y : G} (h : x H) :
          x + y H y 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
            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
              @[simp]
              theorem InvMemClass.coe_inv {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] (x : H) :
              x⁻¹ = (↑x)⁻¹
              @[simp]
              theorem NegMemClass.coe_neg {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : H) :
              ↑(-x) = -x
              theorem SubgroupClass.subset_union {G : Type u_1} [Group G] {S : Type u_4} [SetLike S G] [SubgroupClass S G] {H K L : S} :
              H K L H K H L
              theorem AddSubgroupClass.subset_union {G : Type u_1} [AddGroup G] {S : Type u_4} [SetLike S G] [AddSubgroupClass S G] {H K L : S} :
              H K L H K H L
              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
                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
                  instance AddSubgroupClass.zsmul {M : Type u_5} {S : Type u_6} [SubNegMonoid M] [SetLike S M] [AddSubgroupClass S M] {H : S} :
                  SMul H

                  An additive subgroup of an AddGroup inherits an integer scaling.

                  Equations
                    instance SubgroupClass.zpow {M : Type u_5} {S : Type u_6} [DivInvMonoid M] [SetLike S M] [SubgroupClass S M] {H : S} :
                    Pow H

                    A subgroup of a group inherits an integer power.

                    Equations
                      @[simp]
                      theorem SubgroupClass.coe_div {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] (x y : H) :
                      ↑(x / y) = x / y
                      @[simp]
                      theorem AddSubgroupClass.coe_sub {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] (x y : H) :
                      ↑(x - y) = x - y
                      @[instance 75]
                      instance SubgroupClass.toGroup {G : Type u_1} [Group G] {S : Type u_4} (H : S) [SetLike S G] [SubgroupClass S G] :
                      Group H

                      A subgroup of a group inherits a group structure.

                      Equations
                        @[instance 75]
                        instance AddSubgroupClass.toAddGroup {G : Type u_1} [AddGroup G] {S : Type u_4} (H : S) [SetLike S G] [AddSubgroupClass S G] :

                        An additive subgroup of an AddGroup inherits an AddGroup structure.

                        Equations
                          @[instance 75]
                          instance SubgroupClass.toCommGroup {S : Type u_4} (H : S) {G : Type u_5} [CommGroup G] [SetLike S G] [SubgroupClass S G] :

                          A subgroup of a CommGroup is a CommGroup.

                          Equations
                            @[instance 75]
                            instance AddSubgroupClass.toAddCommGroup {S : Type u_4} (H : S) {G : Type u_5} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :

                            An additive subgroup of an AddCommGroup is an AddCommGroup.

                            Equations
                              def SubgroupClass.subtype {G : Type u_1} [Group G] {S : Type u_4} (H : S) [SetLike S G] [SubgroupClass S G] :
                              H →* G

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

                              Equations
                                Instances For
                                  def AddSubgroupClass.subtype {G : Type u_1} [AddGroup G] {S : Type u_4} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                                  H →+ G

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

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem SubgroupClass.subtype_apply {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] (x : H) :
                                      H x = x
                                      @[simp]
                                      theorem AddSubgroupClass.subtype_apply {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : H) :
                                      H x = x
                                      theorem SubgroupClass.subtype_injective {G : Type u_1} [Group G] {S : Type u_4} (H : S) [SetLike S G] [SubgroupClass S G] :
                                      theorem AddSubgroupClass.subtype_injective {G : Type u_1} [AddGroup G] {S : Type u_4} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                                      @[simp]
                                      theorem SubgroupClass.coe_subtype {G : Type u_1} [Group G] {S : Type u_4} (H : S) [SetLike S G] [SubgroupClass S G] :
                                      H = Subtype.val
                                      @[simp]
                                      theorem AddSubgroupClass.coe_subtype {G : Type u_1} [AddGroup G] {S : Type u_4} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                                      H = Subtype.val
                                      @[deprecated SubgroupClass.coe_subtype (since := "2025-02-18")]
                                      theorem SubgroupClass.coeSubtype {G : Type u_1} [Group G] {S : Type u_4} (H : S) [SetLike S G] [SubgroupClass S G] :
                                      H = Subtype.val

                                      Alias of SubgroupClass.coe_subtype.

                                      @[deprecated AddSubgroupClass.coe_subtype (since := "2025-02-18")]
                                      theorem AddSubgroupClass.coeSubtype {G : Type u_1} [AddGroup G] {S : Type u_4} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                                      H = Subtype.val

                                      Alias of AddSubgroupClass.coe_subtype.

                                      @[simp]
                                      theorem SubgroupClass.coe_pow {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] (x : H) (n : ) :
                                      ↑(x ^ n) = x ^ n
                                      @[simp]
                                      theorem AddSubgroupClass.coe_nsmul {G : Type u_1} [AddGroup G] {S : Type u_4} {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_4} {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_4} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : H) (n : ) :
                                      ↑(n x) = n x
                                      def SubgroupClass.inclusion {G : Type u_1} [Group G] {S : Type u_4} [SetLike S G] [SubgroupClass S G] {H K : S} (h : H K) :
                                      H →* K

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

                                      Equations
                                        Instances For
                                          def AddSubgroupClass.inclusion {G : Type u_1} [AddGroup G] {S : Type u_4} [SetLike S G] [AddSubgroupClass S G] {H K : S} (h : H K) :
                                          H →+ K

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

                                          Equations
                                            Instances For
                                              @[simp]
                                              theorem SubgroupClass.inclusion_self {G : Type u_1} [Group G] {S : Type u_4} {H : S} [SetLike S G] [SubgroupClass S G] (x : H) :
                                              (inclusion ) x = x
                                              @[simp]
                                              theorem AddSubgroupClass.inclusion_self {G : Type u_1} [AddGroup G] {S : Type u_4} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : H) :
                                              (inclusion ) x = x
                                              @[simp]
                                              theorem SubgroupClass.inclusion_mk {G : Type u_1} [Group G] {S : Type u_4} {H K : S} [SetLike S G] [SubgroupClass S G] {h : H K} (x : G) (hx : x H) :
                                              (inclusion h) x, hx = x,
                                              @[simp]
                                              theorem AddSubgroupClass.inclusion_mk {G : Type u_1} [AddGroup G] {S : Type u_4} {H K : S} [SetLike S G] [AddSubgroupClass S G] {h : H K} (x : G) (hx : x H) :
                                              (inclusion h) x, hx = x,
                                              theorem SubgroupClass.inclusion_right {G : Type u_1} [Group G] {S : Type u_4} {H K : S} [SetLike S G] [SubgroupClass S G] (h : H K) (x : K) (hx : x H) :
                                              (inclusion h) x, hx = x
                                              theorem AddSubgroupClass.inclusion_right {G : Type u_1} [AddGroup G] {S : Type u_4} {H K : S} [SetLike S G] [AddSubgroupClass S G] (h : H K) (x : K) (hx : x H) :
                                              (inclusion h) x, hx = x
                                              @[simp]
                                              theorem SubgroupClass.inclusion_inclusion {G : Type u_1} [Group G] {S : Type u_4} {H K : S} [SetLike S G] [SubgroupClass S G] {L : S} (hHK : H K) (hKL : K L) (x : H) :
                                              (inclusion hKL) ((inclusion hHK) x) = (inclusion ) x
                                              @[simp]
                                              theorem SubgroupClass.coe_inclusion {G : Type u_1} [Group G] {S : Type u_4} [SetLike S G] [SubgroupClass S G] {H K : S} {h : H K} (a : H) :
                                              ((inclusion h) a) = a
                                              @[simp]
                                              theorem AddSubgroupClass.coe_inclusion {G : Type u_1} [AddGroup G] {S : Type u_4} [SetLike S G] [AddSubgroupClass S G] {H K : S} {h : H K} (a : H) :
                                              ((inclusion h) a) = a
                                              @[simp]
                                              theorem SubgroupClass.subtype_comp_inclusion {G : Type u_1} [Group G] {S : Type u_4} [SetLike S G] [SubgroupClass S G] {H K : S} (hH : H K) :
                                              (↑K).comp (inclusion hH) = H
                                              @[simp]
                                              theorem AddSubgroupClass.subtype_comp_inclusion {G : Type u_1} [AddGroup G] {S : Type u_4} [SetLike S G] [AddSubgroupClass S G] {H K : S} (hH : H K) :
                                              (↑K).comp (inclusion hH) = H
                                              structure Subgroup (G : Type u_3) [Group G] extends Submonoid G :
                                              Type u_3

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

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

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

                                                Instances For
                                                  instance Subgroup.instSetLike {G : Type u_1} [Group G] :
                                                  Equations
                                                    Equations
                                                      def Subgroup.ofClass {S : Type u_3} {G : Type u_4} [Group G] [SetLike S G] [SubgroupClass S G] (s : S) :

                                                      The actual Subgroup obtained from an element of a SubgroupClass

                                                      Equations
                                                        Instances For
                                                          def AddSubgroup.ofClass {S : Type u_3} {G : Type u_4} [AddGroup G] [SetLike S G] [AddSubgroupClass S G] (s : S) :

                                                          The actual AddSubgroup obtained from an element of a AddSubgroupClass

                                                          Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem AddSubgroup.coe_ofClass {S : Type u_3} {G : Type u_4} [AddGroup G] [SetLike S G] [AddSubgroupClass S G] (s : S) :
                                                              (ofClass s) = s
                                                              @[simp]
                                                              theorem Subgroup.coe_ofClass {S : Type u_3} {G : Type u_4} [Group G] [SetLike S G] [SubgroupClass S G] (s : S) :
                                                              (ofClass s) = s
                                                              @[instance 100]
                                                              instance Subgroup.instCanLiftSetCoeAndMemOfNatForallForallForallForallHMulForallForallInv {G : Type u_1} [Group G] :
                                                              CanLift (Set G) (Subgroup G) SetLike.coe fun (s : Set G) => 1 s (∀ {x y : G}, x sy sx * y s) ∀ {x : G}, x sx⁻¹ s
                                                              @[instance 100]
                                                              instance AddSubgroup.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallNeg {G : Type u_1} [AddGroup G] :
                                                              CanLift (Set G) (AddSubgroup G) SetLike.coe fun (s : Set G) => 0 s (∀ {x y : G}, x sy sx + y s) ∀ {x : G}, x s-x s
                                                              theorem Subgroup.mem_carrier {G : Type u_1} [Group G] {s : Subgroup G} {x : G} :
                                                              x s.carrier x s
                                                              theorem AddSubgroup.mem_carrier {G : Type u_1} [AddGroup G] {s : AddSubgroup G} {x : G} :
                                                              x s.carrier 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 { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrierx⁻¹ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier) :
                                                              x { carrier := s, mul_mem' := h_one, one_mem' := h_mul, inv_mem' := h_inv } x s
                                                              @[simp]
                                                              theorem AddSubgroup.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 { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier-x { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier) :
                                                              x { carrier := s, add_mem' := h_one, zero_mem' := h_mul, neg_mem' := h_inv } x s
                                                              @[simp]
                                                              theorem Subgroup.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 { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrierx⁻¹ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier) :
                                                              { carrier := s, mul_mem' := h_one, one_mem' := h_mul, inv_mem' := h_inv } = s
                                                              @[simp]
                                                              theorem AddSubgroup.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 { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier-x { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier) :
                                                              { carrier := s, add_mem' := h_one, zero_mem' := h_mul, neg_mem' := h_inv } = s
                                                              @[simp]
                                                              theorem Subgroup.mk_le_mk {G : Type u_1} [Group G] {s t : Set G} (h_one : ∀ {a b : G}, a sb sa * b s) (h_mul : s 1) (h_inv : ∀ {x : G}, x { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrierx⁻¹ { carrier := s, mul_mem' := h_one, one_mem' := h_mul }.carrier) (h_one' : ∀ {a b : G}, a tb ta * b t) (h_mul' : t 1) (h_inv' : ∀ {x : G}, x { carrier := t, mul_mem' := h_one', one_mem' := h_mul' }.carrierx⁻¹ { carrier := t, mul_mem' := h_one', one_mem' := h_mul' }.carrier) :
                                                              { carrier := s, mul_mem' := h_one, one_mem' := h_mul, inv_mem' := h_inv } { carrier := t, mul_mem' := h_one', one_mem' := h_mul', inv_mem' := h_inv' } s t
                                                              @[simp]
                                                              theorem AddSubgroup.mk_le_mk {G : Type u_1} [AddGroup G] {s t : Set G} (h_one : ∀ {a b : G}, a sb sa + b s) (h_mul : s 0) (h_inv : ∀ {x : G}, x { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier-x { carrier := s, add_mem' := h_one, zero_mem' := h_mul }.carrier) (h_one' : ∀ {a b : G}, a tb ta + b t) (h_mul' : t 0) (h_inv' : ∀ {x : G}, x { carrier := t, add_mem' := h_one', zero_mem' := h_mul' }.carrier-x { carrier := t, add_mem' := h_one', zero_mem' := h_mul' }.carrier) :
                                                              { carrier := s, add_mem' := h_one, zero_mem' := h_mul, neg_mem' := h_inv } { carrier := t, add_mem' := h_one', zero_mem' := h_mul', neg_mem' := h_inv' } s t
                                                              @[simp]
                                                              theorem Subgroup.coe_toSubmonoid {G : Type u_1} [Group G] (K : Subgroup G) :
                                                              K.toSubmonoid = K
                                                              @[simp]
                                                              theorem AddSubgroup.coe_toAddSubmonoid {G : Type u_1} [AddGroup G] (K : AddSubgroup G) :
                                                              K.toAddSubmonoid = K
                                                              @[simp]
                                                              theorem Subgroup.mem_toSubmonoid {G : Type u_1} [Group G] (K : Subgroup G) (x : G) :
                                                              @[simp]
                                                              theorem AddSubgroup.mem_toAddSubmonoid {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (x : G) :
                                                              @[simp]
                                                              theorem Subgroup.toSubmonoid_inj {G : Type u_1} [Group G] {p q : Subgroup G} :
                                                              @[deprecated Subgroup.toSubmonoid_inj (since := "2024-12-29")]
                                                              theorem Subgroup.toSubmonoid_eq {G : Type u_1} [Group G] {p q : Subgroup G} :

                                                              Alias of Subgroup.toSubmonoid_inj.

                                                              @[simp]
                                                              theorem Subgroup.toSubmonoid_le {G : Type u_1} [Group G] {p q : Subgroup G} :
                                                              @[simp]
                                                              theorem Subgroup.coe_nonempty {G : Type u_1} [Group G] (s : Subgroup G) :
                                                              (↑s).Nonempty
                                                              @[simp]
                                                              theorem AddSubgroup.coe_nonempty {G : Type u_1} [AddGroup G] (s : AddSubgroup G) :
                                                              (↑s).Nonempty
                                                              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
                                                                Instances For
                                                                  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
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem Subgroup.coe_copy {G : Type u_1} [Group G] (K : Subgroup G) (s : Set G) (hs : s = K) :
                                                                      (K.copy s hs) = s
                                                                      @[simp]
                                                                      theorem AddSubgroup.coe_copy {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :
                                                                      (K.copy s hs) = s
                                                                      theorem Subgroup.copy_eq {G : Type u_1} [Group G] (K : Subgroup G) (s : Set G) (hs : s = K) :
                                                                      K.copy s hs = K
                                                                      theorem AddSubgroup.copy_eq {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :
                                                                      K.copy s hs = K
                                                                      theorem Subgroup.ext {G : Type u_1} [Group G] {H K : Subgroup G} (h : ∀ (x : G), x H x K) :
                                                                      H = K

                                                                      Two subgroups are equal if they have the same elements.

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

                                                                      Two AddSubgroups are equal if they have the same elements.

                                                                      theorem AddSubgroup.ext_iff {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} :
                                                                      H = K ∀ (x : G), x H x K
                                                                      theorem Subgroup.ext_iff {G : Type u_1} [Group G] {H K : Subgroup G} :
                                                                      H = K ∀ (x : G), x H x K
                                                                      theorem Subgroup.one_mem {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                      1 H

                                                                      A subgroup contains the group's 1.

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

                                                                      An AddSubgroup contains the group's 0.

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

                                                                      A subgroup is closed under multiplication.

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

                                                                      An AddSubgroup is closed under addition.

                                                                      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.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.div_mem {G : Type u_1} [Group G] (H : Subgroup G) {x y : G} (hx : x H) (hy : y H) :
                                                                      x / y H

                                                                      A subgroup is closed under division.

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

                                                                      An AddSubgroup is closed under subtraction.

                                                                      theorem Subgroup.inv_mem_iff {G : Type u_1} [Group G] (H : Subgroup G) {x : G} :
                                                                      x⁻¹ H x H
                                                                      theorem AddSubgroup.neg_mem_iff {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x : G} :
                                                                      -x H x H
                                                                      theorem Subgroup.exists_inv_mem_iff_exists_mem {G : Type u_1} [Group G] (K : Subgroup G) {P : GProp} :
                                                                      (∃ xK, P x⁻¹) xK, P x
                                                                      theorem AddSubgroup.exists_neg_mem_iff_exists_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {P : GProp} :
                                                                      (∃ xK, P (-x)) xK, P x
                                                                      theorem Subgroup.mul_mem_cancel_right {G : Type u_1} [Group G] (H : Subgroup G) {x y : G} (h : x H) :
                                                                      y * x H y H
                                                                      theorem AddSubgroup.add_mem_cancel_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x y : G} (h : x H) :
                                                                      y + x H y H
                                                                      theorem Subgroup.mul_mem_cancel_left {G : Type u_1} [Group G] (H : Subgroup G) {x y : G} (h : x H) :
                                                                      x * y H y H
                                                                      theorem AddSubgroup.add_mem_cancel_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {x y : G} (h : x H) :
                                                                      x + y H y H
                                                                      theorem Subgroup.pow_mem {G : Type u_1} [Group G] (K : Subgroup G) {x : G} (hx : x K) (n : ) :
                                                                      x ^ n K
                                                                      theorem AddSubgroup.nsmul_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {x : G} (hx : x K) (n : ) :
                                                                      n x K
                                                                      theorem Subgroup.zpow_mem {G : Type u_1} [Group G] (K : Subgroup G) {x : G} (hx : x K) (n : ) :
                                                                      x ^ n K
                                                                      theorem AddSubgroup.zsmul_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {x : G} (hx : x K) (n : ) :
                                                                      n x K
                                                                      def Subgroup.ofDiv {G : Type u_1} [Group G] (s : Set G) (hsn : s.Nonempty) (hs : xs, ys, x * y⁻¹ s) :

                                                                      Construct a subgroup from a nonempty set that is closed under division.

                                                                      Equations
                                                                        Instances For
                                                                          def AddSubgroup.ofSub {G : Type u_1} [AddGroup G] (s : Set G) (hsn : s.Nonempty) (hs : xs, ys, x + -y s) :

                                                                          Construct a subgroup from a nonempty set that is closed under subtraction

                                                                          Equations
                                                                            Instances For
                                                                              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.add {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                                                Add H

                                                                                An AddSubgroup of an AddGroup inherits an addition.

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

                                                                                    An AddSubgroup of an AddGroup inherits a zero.

                                                                                    Equations
                                                                                      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.neg {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                                                        Neg H

                                                                                        An AddSubgroup of an AddGroup inherits an inverse.

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

                                                                                          A subgroup of a group inherits a division

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

                                                                                            An AddSubgroup of an AddGroup inherits a subtraction.

                                                                                            Equations
                                                                                              instance AddSubgroup.nsmul {G : Type u_3} [AddGroup G] {H : AddSubgroup G} :
                                                                                              SMul H

                                                                                              An AddSubgroup of an AddGroup inherits a natural scaling.

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

                                                                                                A subgroup of a group inherits a natural power

                                                                                                Equations
                                                                                                  instance AddSubgroup.zsmul {G : Type u_3} [AddGroup G] {H : AddSubgroup G} :
                                                                                                  SMul H

                                                                                                  An AddSubgroup of an AddGroup inherits an integer scaling.

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

                                                                                                    A subgroup of a group inherits an integer power

                                                                                                    Equations
                                                                                                      @[simp]
                                                                                                      theorem Subgroup.coe_mul {G : Type u_1} [Group G] (H : Subgroup G) (x y : H) :
                                                                                                      ↑(x * y) = x * y
                                                                                                      @[simp]
                                                                                                      theorem AddSubgroup.coe_add {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x y : H) :
                                                                                                      ↑(x + y) = x + y
                                                                                                      @[simp]
                                                                                                      theorem Subgroup.coe_one {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                                      1 = 1
                                                                                                      @[simp]
                                                                                                      theorem AddSubgroup.coe_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                                                                      0 = 0
                                                                                                      @[simp]
                                                                                                      theorem Subgroup.coe_inv {G : Type u_1} [Group G] (H : Subgroup G) (x : H) :
                                                                                                      x⁻¹ = (↑x)⁻¹
                                                                                                      @[simp]
                                                                                                      theorem AddSubgroup.coe_neg {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : H) :
                                                                                                      ↑(-x) = -x
                                                                                                      @[simp]
                                                                                                      theorem Subgroup.coe_div {G : Type u_1} [Group G] (H : Subgroup G) (x y : H) :
                                                                                                      ↑(x / y) = x / y
                                                                                                      @[simp]
                                                                                                      theorem AddSubgroup.coe_sub {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x y : H) :
                                                                                                      ↑(x - y) = x - y
                                                                                                      theorem Subgroup.coe_mk {G : Type u_1} [Group G] (H : Subgroup G) (x : G) (hx : x H) :
                                                                                                      x, hx = x
                                                                                                      theorem AddSubgroup.coe_mk {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : G) (hx : x H) :
                                                                                                      x, hx = x
                                                                                                      @[simp]
                                                                                                      theorem Subgroup.coe_pow {G : Type u_1} [Group G] (H : Subgroup G) (x : H) (n : ) :
                                                                                                      ↑(x ^ n) = x ^ n
                                                                                                      @[simp]
                                                                                                      theorem AddSubgroup.coe_nsmul {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
                                                                                                      theorem AddSubgroup.coe_zsmul {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : H) (n : ) :
                                                                                                      ↑(n x) = n x
                                                                                                      @[simp]
                                                                                                      theorem Subgroup.mk_eq_one {G : Type u_1} [Group G] (H : Subgroup G) {g : G} {h : g H} :
                                                                                                      g, h = 1 g = 1
                                                                                                      @[simp]
                                                                                                      theorem AddSubgroup.mk_eq_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {g : G} {h : g H} :
                                                                                                      g, h = 0 g = 0
                                                                                                      instance Subgroup.toGroup {G : Type u_3} [Group G] (H : Subgroup G) :
                                                                                                      Group H

                                                                                                      A subgroup of a group inherits a group structure.

                                                                                                      Equations
                                                                                                        instance AddSubgroup.toAddGroup {G : Type u_3} [AddGroup G] (H : AddSubgroup G) :

                                                                                                        An AddSubgroup of an AddGroup inherits an AddGroup structure.

                                                                                                        Equations
                                                                                                          instance Subgroup.toCommGroup {G : Type u_3} [CommGroup G] (H : Subgroup G) :

                                                                                                          A subgroup of a CommGroup is a CommGroup.

                                                                                                          Equations
                                                                                                            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
                                                                                                              Instances For
                                                                                                                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
                                                                                                                  Instances For
                                                                                                                    @[simp]
                                                                                                                    theorem Subgroup.subtype_apply {G : Type u_1} [Group G] {s : Subgroup G} (x : s) :
                                                                                                                    s.subtype x = x
                                                                                                                    @[simp]
                                                                                                                    theorem AddSubgroup.subtype_apply {G : Type u_1} [AddGroup G] {s : AddSubgroup G} (x : s) :
                                                                                                                    s.subtype x = x
                                                                                                                    @[simp]
                                                                                                                    theorem Subgroup.coe_subtype {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                                                    @[simp]
                                                                                                                    @[deprecated Subgroup.coe_subtype (since := "2025-02-18")]
                                                                                                                    theorem Subgroup.coeSubtype {G : Type u_1} [Group G] (H : Subgroup G) :

                                                                                                                    Alias of Subgroup.coe_subtype.

                                                                                                                    @[deprecated AddSubgroup.coe_subtype (since := "2025-02-18")]

                                                                                                                    Alias of AddSubgroup.coe_subtype.

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

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

                                                                                                                    Equations
                                                                                                                      Instances For
                                                                                                                        def AddSubgroup.inclusion {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H K) :
                                                                                                                        H →+ K

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

                                                                                                                        Equations
                                                                                                                          Instances For
                                                                                                                            @[simp]
                                                                                                                            theorem Subgroup.coe_inclusion {G : Type u_1} [Group G] {H K : Subgroup G} {h : H K} (a : H) :
                                                                                                                            ((inclusion h) a) = a
                                                                                                                            @[simp]
                                                                                                                            theorem AddSubgroup.coe_inclusion {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} {h : H K} (a : H) :
                                                                                                                            ((inclusion h) a) = a
                                                                                                                            theorem Subgroup.inclusion_injective {G : Type u_1} [Group G] {H K : Subgroup G} (h : H K) :
                                                                                                                            @[simp]
                                                                                                                            theorem Subgroup.inclusion_inj {G : Type u_1} [Group G] {H K : Subgroup G} (h : H K) {x y : H} :
                                                                                                                            (inclusion h) x = (inclusion h) y x = y
                                                                                                                            @[simp]
                                                                                                                            theorem AddSubgroup.inclusion_inj {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H K) {x y : H} :
                                                                                                                            (inclusion h) x = (inclusion h) y x = y
                                                                                                                            @[simp]
                                                                                                                            theorem Subgroup.subtype_comp_inclusion {G : Type u_1} [Group G] {H K : Subgroup G} (hH : H K) :
                                                                                                                            @[simp]
                                                                                                                            theorem AddSubgroup.subtype_comp_inclusion {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (hH : H K) :
                                                                                                                            class Subgroup.Normal {G : Type u_1} [Group G] (H : Subgroup G) :

                                                                                                                            A subgroup is normal if whenever n ∈ H, then g * n * g⁻¹ ∈ H for every g : G

                                                                                                                            • conj_mem (n : G) : n H∀ (g : G), g * n * g⁻¹ H

                                                                                                                              N is closed under conjugation

                                                                                                                            Instances
                                                                                                                              class AddSubgroup.Normal {A : Type u_2} [AddGroup A] (H : AddSubgroup A) :

                                                                                                                              An AddSubgroup is normal if whenever n ∈ H, then g + n - g ∈ H for every g : G

                                                                                                                              • conj_mem (n : A) : n H∀ (g : A), g + n + -g H

                                                                                                                                N is closed under additive conjugation

                                                                                                                              Instances
                                                                                                                                @[instance 100]
                                                                                                                                instance Subgroup.normal_of_comm {G : Type u_3} [CommGroup G] (H : Subgroup G) :
                                                                                                                                @[instance 100]
                                                                                                                                theorem Subgroup.Normal.conj_mem' {G : Type u_1} [Group G] {H : Subgroup G} (nH : H.Normal) (n : G) (hn : n H) (g : G) :
                                                                                                                                g⁻¹ * n * g H
                                                                                                                                theorem AddSubgroup.Normal.conj_mem' {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (nH : H.Normal) (n : G) (hn : n H) (g : G) :
                                                                                                                                -g + n + g H
                                                                                                                                theorem Subgroup.Normal.mem_comm {G : Type u_1} [Group G] {H : Subgroup G} (nH : H.Normal) {a b : G} (h : a * b H) :
                                                                                                                                b * a H
                                                                                                                                theorem AddSubgroup.Normal.mem_comm {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (nH : H.Normal) {a b : G} (h : a + b H) :
                                                                                                                                b + a H
                                                                                                                                theorem Subgroup.Normal.mem_comm_iff {G : Type u_1} [Group G] {H : Subgroup G} (nH : H.Normal) {a b : G} :
                                                                                                                                a * b H b * a H
                                                                                                                                theorem AddSubgroup.Normal.mem_comm_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (nH : H.Normal) {a b : G} :
                                                                                                                                a + b H b + a H
                                                                                                                                def Subgroup.normalizer {G : Type u_1} [Group G] (H : Subgroup G) :

                                                                                                                                The normalizer of H is the largest subgroup of G inside which H is normal.

                                                                                                                                Equations
                                                                                                                                  Instances For

                                                                                                                                    The normalizer of H is the largest subgroup of G inside which H is normal.

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

                                                                                                                                        The setNormalizer of S is the subgroup of G whose elements satisfy g*S*g⁻¹=S

                                                                                                                                        Equations
                                                                                                                                          Instances For

                                                                                                                                            The setNormalizer of S is the subgroup of G whose elements satisfy g+S-g=S.

                                                                                                                                            Equations
                                                                                                                                              Instances For
                                                                                                                                                theorem Subgroup.mem_normalizer_iff {G : Type u_1} [Group G] {H : Subgroup G} {g : G} :
                                                                                                                                                g H.normalizer ∀ (h : G), h H g * h * g⁻¹ H
                                                                                                                                                theorem AddSubgroup.mem_normalizer_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {g : G} :
                                                                                                                                                g H.normalizer ∀ (h : G), h H g + h + -g H
                                                                                                                                                theorem Subgroup.mem_normalizer_iff'' {G : Type u_1} [Group G] {H : Subgroup G} {g : G} :
                                                                                                                                                g H.normalizer ∀ (h : G), h H g⁻¹ * h * g H
                                                                                                                                                theorem AddSubgroup.mem_normalizer_iff'' {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {g : G} :
                                                                                                                                                g H.normalizer ∀ (h : G), h H -g + h + g H
                                                                                                                                                theorem Subgroup.mem_normalizer_iff' {G : Type u_1} [Group G] {H : Subgroup G} {g : G} :
                                                                                                                                                g H.normalizer ∀ (n : G), n * g H g * n H
                                                                                                                                                theorem AddSubgroup.mem_normalizer_iff' {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {g : G} :
                                                                                                                                                g H.normalizer ∀ (n : G), n + g H g + n H
                                                                                                                                                theorem Subgroup.le_normalizer {G : Type u_1} [Group G] {H : Subgroup G} :
                                                                                                                                                @[deprecated IsMulCommutative (since := "2025-04-09")]
                                                                                                                                                def Subgroup.IsCommutative (M : Type u_2) [Mul M] :

                                                                                                                                                Alias of IsMulCommutative.


                                                                                                                                                A Prop stating that the multiplication is commutative.

                                                                                                                                                Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[deprecated IsAddCommutative (since := "2025-04-09")]

                                                                                                                                                    Alias of IsAddCommutative.


                                                                                                                                                    A Prop stating that the addition is commutative.

                                                                                                                                                    Equations
                                                                                                                                                      Instances For

                                                                                                                                                        A subgroup of a commutative group is commutative.

                                                                                                                                                        A subgroup of a commutative group is commutative.

                                                                                                                                                        @[deprecated Subgroup.commGroup_isMulCommutative (since := "2025-04-09")]

                                                                                                                                                        Alias of Subgroup.commGroup_isMulCommutative.


                                                                                                                                                        A subgroup of a commutative group is commutative.

                                                                                                                                                        @[deprecated Subgroup.commGroup_isMulCommutative (since := "2025-04-09")]

                                                                                                                                                        Alias of Subgroup.commGroup_isMulCommutative.


                                                                                                                                                        A subgroup of a commutative group is commutative.

                                                                                                                                                        theorem Subgroup.mul_comm_of_mem_isMulCommutative {G : Type u_1} [Group G] (H : Subgroup G) [IsMulCommutative H] {a b : G} (ha : a H) (hb : b H) :
                                                                                                                                                        a * b = b * a
                                                                                                                                                        theorem AddSubgroup.add_comm_of_mem_isAddCommutative {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [IsAddCommutative H] {a b : G} (ha : a H) (hb : b H) :
                                                                                                                                                        a + b = b + a
                                                                                                                                                        @[deprecated Subgroup.mul_comm_of_mem_isMulCommutative (since := "2025-04-09")]
                                                                                                                                                        theorem Subgroup.mul_comm_of_mem_isCommutative {G : Type u_1} [Group G] (H : Subgroup G) [IsMulCommutative H] {a b : G} (ha : a H) (hb : b H) :
                                                                                                                                                        a * b = b * a

                                                                                                                                                        Alias of Subgroup.mul_comm_of_mem_isMulCommutative.

                                                                                                                                                        @[deprecated AddSubgroup.add_comm_of_mem_isAddCommutative (since := "2025-04-09")]
                                                                                                                                                        theorem AddSubgroup.add_comm_of_mem_isCommutative {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [IsAddCommutative H] {a b : G} (ha : a H) (hb : b H) :
                                                                                                                                                        a + b = b + a

                                                                                                                                                        Alias of AddSubgroup.add_comm_of_mem_isAddCommutative.