Documentation

Mathlib.Algebra.Group.Subgroup.Lattice

Lattice structure of subgroups #

We prove subgroups of a group form a complete lattice.

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

Conversion to/from Additive/Multiplicative #

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

Equations
    Instances For
      @[simp]
      @[reducible, inline]

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

      Equations
        Instances For

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

          Equations
            Instances For
              @[reducible, inline]

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

              Equations
                Instances For
                  instance Subgroup.instTop {G : Type u_1} [Group G] :

                  The subgroup G of the group G.

                  Equations
                    instance AddSubgroup.instTop {G : Type u_1} [AddGroup G] :

                    The AddSubgroup G of the AddGroup G.

                    Equations
                      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
                        Instances For
                          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
                            Instances For
                              @[simp]
                              theorem AddSubgroup.topEquiv_symm_apply_coe {G : Type u_1} [AddGroup G] (x : G) :
                              (topEquiv.symm x) = x
                              @[simp]
                              theorem Subgroup.topEquiv_apply {G : Type u_1} [Group G] (x : ) :
                              topEquiv x = x
                              @[simp]
                              theorem AddSubgroup.topEquiv_apply {G : Type u_1} [AddGroup G] (x : ) :
                              topEquiv x = x
                              @[simp]
                              theorem Subgroup.topEquiv_symm_apply_coe {G : Type u_1} [Group G] (x : G) :
                              (topEquiv.symm x) = x
                              instance Subgroup.instBot {G : Type u_1} [Group G] :

                              The trivial subgroup {1} of a group G.

                              Equations
                                instance AddSubgroup.instBot {G : Type u_1} [AddGroup G] :

                                The trivial AddSubgroup {0} of an AddGroup G.

                                Equations
                                  instance Subgroup.instInhabited {G : Type u_1} [Group G] :
                                  Equations
                                    @[simp]
                                    theorem Subgroup.mem_bot {G : Type u_1} [Group G] {x : G} :
                                    x x = 1
                                    @[simp]
                                    theorem AddSubgroup.mem_bot {G : Type u_1} [AddGroup G] {x : G} :
                                    x x = 0
                                    @[simp]
                                    theorem Subgroup.mem_top {G : Type u_1} [Group G] (x : G) :
                                    @[simp]
                                    theorem AddSubgroup.mem_top {G : Type u_1} [AddGroup G] (x : G) :
                                    @[simp]
                                    theorem Subgroup.coe_top {G : Type u_1} [Group G] :
                                    @[simp]
                                    theorem AddSubgroup.coe_top {G : Type u_1} [AddGroup G] :
                                    @[simp]
                                    theorem Subgroup.coe_bot {G : Type u_1} [Group G] :
                                    = {1}
                                    @[simp]
                                    theorem AddSubgroup.coe_bot {G : Type u_1} [AddGroup G] :
                                    = {0}
                                    Equations
                                      theorem Subgroup.eq_bot_iff_forall {G : Type u_1} [Group G] (H : Subgroup G) :
                                      H = xH, x = 1
                                      theorem AddSubgroup.eq_bot_iff_forall {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                      H = xH, x = 0
                                      @[simp]
                                      theorem Subgroup.coe_eq_univ {G : Type u_1} [Group G] {H : Subgroup G} :
                                      H = Set.univ H =
                                      @[simp]
                                      theorem AddSubgroup.coe_eq_univ {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                      H = Set.univ H =
                                      theorem Subgroup.coe_eq_singleton {G : Type u_1} [Group G] {H : Subgroup G} :
                                      (∃ (g : G), H = {g}) H =
                                      theorem AddSubgroup.coe_eq_singleton {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                      (∃ (g : G), H = {g}) H =
                                      theorem Subgroup.nontrivial_iff_exists_ne_one {G : Type u_1} [Group G] (H : Subgroup G) :
                                      Nontrivial H xH, x 1
                                      theorem AddSubgroup.nontrivial_iff_exists_ne_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                      Nontrivial H xH, x 0
                                      theorem Subgroup.exists_ne_one_of_nontrivial {G : Type u_1} [Group G] (H : Subgroup G) [Nontrivial H] :
                                      xH, x 1
                                      theorem AddSubgroup.exists_ne_zero_of_nontrivial {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Nontrivial H] :
                                      xH, x 0
                                      theorem Subgroup.bot_or_nontrivial {G : Type u_1} [Group G] (H : Subgroup G) :

                                      A subgroup is either the trivial subgroup or nontrivial.

                                      A subgroup is either the trivial subgroup or nontrivial.

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

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

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

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

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

                                      The inf of two subgroups is their intersection.

                                      Equations
                                        instance AddSubgroup.instMin {G : Type u_1} [AddGroup G] :

                                        The inf of two AddSubgroups is their intersection.

                                        Equations
                                          @[simp]
                                          theorem Subgroup.coe_inf {G : Type u_1} [Group G] (p p' : Subgroup G) :
                                          (pp') = p p'
                                          @[simp]
                                          theorem AddSubgroup.coe_inf {G : Type u_1} [AddGroup G] (p p' : AddSubgroup G) :
                                          (pp') = p p'
                                          @[simp]
                                          theorem Subgroup.mem_inf {G : Type u_1} [Group G] {p p' : Subgroup G} {x : G} :
                                          x pp' x p x p'
                                          @[simp]
                                          theorem AddSubgroup.mem_inf {G : Type u_1} [AddGroup G] {p p' : AddSubgroup G} {x : G} :
                                          x pp' x p x p'
                                          instance Subgroup.instInfSet {G : Type u_1} [Group G] :
                                          Equations
                                            Equations
                                              @[simp]
                                              theorem Subgroup.coe_sInf {G : Type u_1} [Group G] (H : Set (Subgroup G)) :
                                              (sInf H) = sH, s
                                              @[simp]
                                              theorem AddSubgroup.coe_sInf {G : Type u_1} [AddGroup G] (H : Set (AddSubgroup G)) :
                                              (sInf H) = sH, s
                                              @[simp]
                                              theorem Subgroup.mem_sInf {G : Type u_1} [Group G] {S : Set (Subgroup G)} {x : G} :
                                              x sInf S pS, x p
                                              @[simp]
                                              theorem AddSubgroup.mem_sInf {G : Type u_1} [AddGroup G] {S : Set (AddSubgroup G)} {x : G} :
                                              x sInf S pS, x p
                                              theorem Subgroup.mem_iInf {G : Type u_1} [Group G] {ι : Sort u_2} {S : ιSubgroup G} {x : G} :
                                              x ⨅ (i : ι), S i ∀ (i : ι), x S i
                                              theorem AddSubgroup.mem_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_2} {S : ιAddSubgroup G} {x : G} :
                                              x ⨅ (i : ι), S i ∀ (i : ι), x S i
                                              @[simp]
                                              theorem Subgroup.coe_iInf {G : Type u_1} [Group G] {ι : Sort u_2} {S : ιSubgroup G} :
                                              (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
                                              @[simp]
                                              theorem AddSubgroup.coe_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_2} {S : ιAddSubgroup G} :
                                              (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)

                                              Subgroups of a group form a complete lattice.

                                              Equations

                                                The AddSubgroups of an AddGroup form a complete lattice.

                                                Equations
                                                  theorem Subgroup.mem_sup_left {G : Type u_1} [Group G] {S T : Subgroup G} {x : G} :
                                                  x Sx ST
                                                  theorem AddSubgroup.mem_sup_left {G : Type u_1} [AddGroup G] {S T : AddSubgroup G} {x : G} :
                                                  x Sx ST
                                                  theorem Subgroup.mem_sup_right {G : Type u_1} [Group G] {S T : Subgroup G} {x : G} :
                                                  x Tx ST
                                                  theorem AddSubgroup.mem_sup_right {G : Type u_1} [AddGroup G] {S T : AddSubgroup G} {x : G} :
                                                  x Tx ST
                                                  theorem Subgroup.mul_mem_sup {G : Type u_1} [Group G] {S T : Subgroup G} {x y : G} (hx : x S) (hy : y T) :
                                                  x * y ST
                                                  theorem AddSubgroup.add_mem_sup {G : Type u_1} [AddGroup G] {S T : AddSubgroup G} {x y : G} (hx : x S) (hy : y T) :
                                                  x + y ST
                                                  theorem Subgroup.mem_iSup_of_mem {G : Type u_1} [Group G] {ι : Sort u_2} {S : ιSubgroup G} (i : ι) {x : G} :
                                                  x S ix iSup S
                                                  theorem AddSubgroup.mem_iSup_of_mem {G : Type u_1} [AddGroup G] {ι : Sort u_2} {S : ιAddSubgroup G} (i : ι) {x : G} :
                                                  x S ix iSup 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
                                                  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.eq_top_iff' {G : Type u_1} [Group G] (H : Subgroup G) :
                                                  H = ∀ (x : G), x H
                                                  theorem AddSubgroup.eq_top_iff' {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                  H = ∀ (x : G), x H
                                                  def Subgroup.closure {G : Type u_1} [Group G] (k : Set G) :

                                                  The Subgroup generated by a set.

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

                                                      The AddSubgroup generated by a set

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

                                                          The subgroup generated by a set includes the set.

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

                                                          The AddSubgroup generated by a set includes the set.

                                                          theorem Subgroup.notMem_of_notMem_closure {G : Type u_1} [Group G] {k : Set G} {P : G} (hP : Pclosure k) :
                                                          Pk
                                                          theorem AddSubgroup.notMem_of_notMem_closure {G : Type u_1} [AddGroup G] {k : Set G} {P : G} (hP : Pclosure k) :
                                                          Pk
                                                          @[deprecated AddSubgroup.notMem_of_notMem_closure (since := "2025-05-23")]
                                                          theorem AddSubgroup.not_mem_of_not_mem_closure {G : Type u_1} [AddGroup G] {k : Set G} {P : G} (hP : Pclosure k) :
                                                          Pk

                                                          Alias of AddSubgroup.notMem_of_notMem_closure.

                                                          @[deprecated Subgroup.notMem_of_notMem_closure (since := "2025-05-23")]
                                                          theorem Subgroup.not_mem_of_not_mem_closure {G : Type u_1} [Group G] {k : Set G} {P : G} (hP : Pclosure k) :
                                                          Pk

                                                          Alias of Subgroup.notMem_of_notMem_closure.

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

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

                                                          @[simp]
                                                          theorem AddSubgroup.closure_le {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {k : Set G} :
                                                          closure k K k K

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

                                                          theorem Subgroup.closure_eq_of_le {G : Type u_1} [Group G] (K : Subgroup G) {k : Set G} (h₁ : k K) (h₂ : K closure k) :
                                                          theorem AddSubgroup.closure_eq_of_le {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {k : Set G} (h₁ : k K) (h₂ : K closure k) :
                                                          theorem Subgroup.closure_induction {G : Type u_1} [Group G] {k : Set G} {p : (g : G) → g closure kProp} (mem : ∀ (x : G) (hx : x k), p x ) (one : p 1 ) (mul : ∀ (x y : G) (hx : x closure k) (hy : y closure k), p x hxp y hyp (x * y) ) (inv : ∀ (x : G) (hx : x closure k), p x hxp x⁻¹ ) {x : G} (hx : x closure k) :
                                                          p x hx

                                                          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.

                                                          See also Subgroup.closure_induction_left and Subgroup.closure_induction_right for versions that only require showing p is preserved by multiplication by elements in k.

                                                          theorem AddSubgroup.closure_induction {G : Type u_1} [AddGroup G] {k : Set G} {p : (g : G) → g closure kProp} (mem : ∀ (x : G) (hx : x k), p x ) (one : p 0 ) (mul : ∀ (x y : G) (hx : x closure k) (hy : y closure k), p x hxp y hyp (x + y) ) (inv : ∀ (x : G) (hx : x closure k), p x hxp (-x) ) {x : G} (hx : x closure k) :
                                                          p x hx

                                                          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.

                                                          See also AddSubgroup.closure_induction_left and AddSubgroup.closure_induction_left for versions that only require showing p is preserved by addition by elements in k.

                                                          theorem Subgroup.closure_induction₂ {G : Type u_1} [Group G] {k : Set G} {p : (x y : G) → x closure ky closure kProp} (mem : ∀ (x y : G) (hx : x k) (hy : y k), p x y ) (one_left : ∀ (x : G) (hx : x closure k), p 1 x hx) (one_right : ∀ (x : G) (hx : x closure k), p x 1 hx ) (mul_left : ∀ (x y z : G) (hx : x closure k) (hy : y closure k) (hz : z closure k), p x z hx hzp y z hy hzp (x * y) z hz) (mul_right : ∀ (y z x : G) (hy : y closure k) (hz : z closure k) (hx : x closure k), p x y hx hyp x z hx hzp x (y * z) hx ) (inv_left : ∀ (x y : G) (hx : x closure k) (hy : y closure k), p x y hx hyp x⁻¹ y hy) (inv_right : ∀ (x y : G) (hx : x closure k) (hy : y closure k), p x y hx hyp x y⁻¹ hx ) {x y : G} (hx : x closure k) (hy : y closure k) :
                                                          p x y hx hy

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

                                                          theorem AddSubgroup.closure_induction₂ {G : Type u_1} [AddGroup G] {k : Set G} {p : (x y : G) → x closure ky closure kProp} (mem : ∀ (x y : G) (hx : x k) (hy : y k), p x y ) (one_left : ∀ (x : G) (hx : x closure k), p 0 x hx) (one_right : ∀ (x : G) (hx : x closure k), p x 0 hx ) (mul_left : ∀ (x y z : G) (hx : x closure k) (hy : y closure k) (hz : z closure k), p x z hx hzp y z hy hzp (x + y) z hz) (mul_right : ∀ (y z x : G) (hy : y closure k) (hz : z closure k) (hx : x closure k), p x y hx hyp x z hx hzp x (y + z) hx ) (inv_left : ∀ (x y : G) (hx : x closure k) (hy : y closure k), p x y hx hyp (-x) y hy) (inv_right : ∀ (x y : G) (hx : x closure k) (hy : y closure k), p x y hx hyp x (-y) hx ) {x y : G} (hx : x closure k) (hy : y closure k) :
                                                          p x y hx hy

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

                                                          closure forms a Galois insertion with the coercion to set.

                                                          Equations
                                                            Instances For

                                                              closure forms a Galois insertion with the coercion to set.

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

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

                                                                  theorem AddSubgroup.closure_mono {G : Type u_1} [AddGroup G] h 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

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

                                                                  Closure of a subgroup K equals K.

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

                                                                  Additive closure of an additive subgroup K equals K

                                                                  @[simp]
                                                                  @[simp]
                                                                  theorem Subgroup.closure_union {G : Type u_1} [Group G] (s t : Set G) :
                                                                  closure (s t) = closure sclosure t
                                                                  theorem AddSubgroup.closure_union {G : Type u_1} [AddGroup G] (s t : Set G) :
                                                                  closure (s t) = closure sclosure t
                                                                  theorem Subgroup.sup_eq_closure {G : Type u_1} [Group G] (H H' : Subgroup G) :
                                                                  HH' = closure (H H')
                                                                  theorem AddSubgroup.sup_eq_closure {G : Type u_1} [AddGroup G] (H H' : AddSubgroup G) :
                                                                  HH' = closure (H H')
                                                                  theorem Subgroup.closure_iUnion {G : Type u_1} [Group G] {ι : Sort u_2} (s : ιSet G) :
                                                                  closure (⋃ (i : ι), s i) = ⨆ (i : ι), closure (s i)
                                                                  theorem AddSubgroup.closure_iUnion {G : Type u_1} [AddGroup G] {ι : Sort u_2} (s : ιSet G) :
                                                                  closure (⋃ (i : ι), s i) = ⨆ (i : ι), closure (s i)
                                                                  @[simp]
                                                                  theorem Subgroup.closure_eq_bot_iff {G : Type u_1} [Group G] {k : Set G} :
                                                                  @[simp]
                                                                  theorem AddSubgroup.closure_eq_bot_iff {G : Type u_1} [AddGroup G] {k : Set G} :
                                                                  theorem Subgroup.iSup_eq_closure {G : Type u_1} [Group G] {ι : Sort u_2} (p : ιSubgroup G) :
                                                                  ⨆ (i : ι), p i = closure (⋃ (i : ι), (p i))
                                                                  theorem AddSubgroup.iSup_eq_closure {G : Type u_1} [AddGroup G] {ι : Sort u_2} (p : ιAddSubgroup G) :
                                                                  ⨆ (i : ι), p i = closure (⋃ (i : ι), (p i))
                                                                  theorem Subgroup.mem_closure_singleton {G : Type u_1} [Group G] {x y : G} :
                                                                  y 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.

                                                                  theorem AddSubgroup.mem_closure_singleton {G : Type u_1} [AddGroup G] {x y : G} :
                                                                  y 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.

                                                                  @[simp]
                                                                  theorem Subgroup.mem_closure_singleton_self {G : Type u_1} [Group G] (x : G) :
                                                                  @[simp]
                                                                  @[simp]
                                                                  theorem Subgroup.closure_insert_one {G : Type u_1} [Group G] (s : Set G) :
                                                                  @[simp]
                                                                  theorem AddSubgroup.closure_insert_zero {G : Type u_1} [AddGroup G] (s : Set G) :
                                                                  theorem Subgroup.mem_iSup_of_directed {G : Type u_1} [Group G] {ι : Sort u_2} [ : Nonempty ι] {K : ιSubgroup G} (hK : Directed (fun (x1 x2 : Subgroup G) => x1 x2) K) {x : G} :
                                                                  x iSup K ∃ (i : ι), x K i
                                                                  theorem AddSubgroup.mem_iSup_of_directed {G : Type u_1} [AddGroup G] {ι : Sort u_2} [ : Nonempty ι] {K : ιAddSubgroup G} (hK : Directed (fun (x1 x2 : AddSubgroup G) => x1 x2) K) {x : G} :
                                                                  x iSup K ∃ (i : ι), x K i
                                                                  theorem Subgroup.coe_iSup_of_directed {G : Type u_1} [Group G] {ι : Sort u_2} [Nonempty ι] {S : ιSubgroup G} (hS : Directed (fun (x1 x2 : Subgroup G) => x1 x2) S) :
                                                                  (⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
                                                                  theorem AddSubgroup.coe_iSup_of_directed {G : Type u_1} [AddGroup G] {ι : Sort u_2} [Nonempty ι] {S : ιAddSubgroup G} (hS : Directed (fun (x1 x2 : AddSubgroup G) => x1 x2) S) :
                                                                  (⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
                                                                  theorem Subgroup.mem_sSup_of_directedOn {G : Type u_1} [Group G] {K : Set (Subgroup G)} (Kne : K.Nonempty) (hK : DirectedOn (fun (x1 x2 : Subgroup G) => x1 x2) K) {x : G} :
                                                                  x sSup K sK, x s
                                                                  theorem AddSubgroup.mem_sSup_of_directedOn {G : Type u_1} [AddGroup G] {K : Set (AddSubgroup G)} (Kne : K.Nonempty) (hK : DirectedOn (fun (x1 x2 : AddSubgroup G) => x1 x2) K) {x : G} :
                                                                  x sSup K sK, x s
                                                                  theorem Subgroup.mem_sup {C : Type u_2} [CommGroup C] {s t : Subgroup C} {x : C} :
                                                                  x st ys, zt, y * z = x
                                                                  theorem AddSubgroup.mem_sup {C : Type u_2} [AddCommGroup C] {s t : AddSubgroup C} {x : C} :
                                                                  x st ys, zt, y + z = x
                                                                  theorem Subgroup.mem_sup' {C : Type u_2} [CommGroup C] {s t : Subgroup C} {x : C} :
                                                                  x st ∃ (y : s) (z : t), y * z = x
                                                                  theorem AddSubgroup.mem_sup' {C : Type u_2} [AddCommGroup C] {s t : AddSubgroup C} {x : C} :
                                                                  x st ∃ (y : s) (z : t), y + z = x
                                                                  theorem Subgroup.mem_closure_pair {C : Type u_2} [CommGroup C] {x y z : C} :
                                                                  z closure {x, y} ∃ (m : ) (n : ), x ^ m * y ^ n = z
                                                                  theorem AddSubgroup.mem_closure_pair {C : Type u_2} [AddCommGroup C] {x y z : C} :
                                                                  z closure {x, y} ∃ (m : ) (n : ), m x + n y = z
                                                                  theorem Subgroup.disjoint_def {G : Type u_1} [Group G] {H₁ H₂ : Subgroup G} :
                                                                  Disjoint H₁ H₂ ∀ {x : G}, x H₁x H₂x = 1
                                                                  theorem AddSubgroup.disjoint_def {G : Type u_1} [AddGroup G] {H₁ H₂ : AddSubgroup G} :
                                                                  Disjoint H₁ H₂ ∀ {x : G}, x H₁x H₂x = 0
                                                                  theorem Subgroup.disjoint_def' {G : Type u_1} [Group G] {H₁ H₂ : Subgroup G} :
                                                                  Disjoint H₁ H₂ ∀ {x y : G}, x H₁y H₂x = yx = 1
                                                                  theorem AddSubgroup.disjoint_def' {G : Type u_1} [AddGroup G] {H₁ H₂ : AddSubgroup G} :
                                                                  Disjoint H₁ H₂ ∀ {x y : G}, x H₁y H₂x = yx = 0
                                                                  theorem Subgroup.disjoint_iff_mul_eq_one {G : Type u_1} [Group G] {H₁ H₂ : Subgroup G} :
                                                                  Disjoint H₁ H₂ ∀ {x y : G}, x H₁y H₂x * y = 1x = 1 y = 1
                                                                  theorem AddSubgroup.disjoint_iff_add_eq_zero {G : Type u_1} [AddGroup G] {H₁ H₂ : AddSubgroup G} :
                                                                  Disjoint H₁ H₂ ∀ {x y : G}, x H₁y H₂x + y = 0x = 0 y = 0
                                                                  theorem Subgroup.mul_injective_of_disjoint {G : Type u_1} [Group G] {H₁ H₂ : Subgroup G} (h : Disjoint H₁ H₂) :
                                                                  Function.Injective fun (g : H₁ × H₂) => g.1 * g.2
                                                                  theorem AddSubgroup.add_injective_of_disjoint {G : Type u_1} [AddGroup G] {H₁ H₂ : AddSubgroup G} (h : Disjoint H₁ H₂) :
                                                                  Function.Injective fun (g : H₁ × H₂) => g.1 + g.2