Documentation

Mathlib.Algebra.Group.Subgroup.Basic

Subgroups #

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

We prove subgroups of a group form a complete lattice, and results about images and preimages of subgroups under group homomorphisms. The bundled subgroups use bundled monoid homomorphisms.

There are also theorems about the subgroups generated by an element or a subset of a group, defined both inductively and as the infimum of the set of subgroups containing a given element/subset.

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

Main definitions #

Notation used here:

Definitions in the file:

Implementation notes #

Subgroup inclusion is denoted rather than , although is defined as membership of a subgroup's underlying set.

Tags #

subgroup, subgroups

class InvMemClass (S : Type u_5) (G : Type u_6) [Inv G] [SetLike S G] :

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

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

    s is closed under inverses

Instances
    theorem InvMemClass.inv_mem {S : Type u_5} {G : Type u_6} [Inv G] [SetLike S G] [self : InvMemClass S G] {s : S} {x : G} :
    x sx⁻¹ s

    s is closed under inverses

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

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

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

      s is closed under negation

    Instances
      theorem NegMemClass.neg_mem {S : Type u_5} {G : Type u_6} [Neg G] [SetLike S G] [self : NegMemClass S G] {s : S} {x : G} :
      x s-x s

      s is closed under negation

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

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

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

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

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

              An additive subgroup is closed under subtraction.

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

              A subgroup is closed under division.

              theorem zsmul_mem {M : Type u_5} {S : Type u_6} [SubNegMonoid M] [SetLike S M] [hSM : AddSubgroupClass S M] {K : S} {x : M} (hx : x K) (n : ) :
              n x K
              theorem zpow_mem {M : Type u_5} {S : Type u_6} [DivInvMonoid M] [SetLike S M] [hSM : SubgroupClass S M] {K : S} {x : M} (hx : x K) (n : ) :
              x ^ n K
              theorem sub_mem_comm_iff {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] {a : G} {b : G} :
              a - b H b - a H
              theorem div_mem_comm_iff {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] {a : G} {b : G} :
              a / b H b / a H
              theorem exists_neg_mem_iff_exists_mem {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] {P : GProp} :
              (∃ xH, P (-x)) xH, P x
              theorem exists_inv_mem_iff_exists_mem {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] {P : GProp} :
              (∃ xH, P x⁻¹) xH, P x
              theorem add_mem_cancel_right {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] {x : G} {y : G} (h : x H) :
              y + x H y H
              theorem mul_mem_cancel_right {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] {x : G} {y : G} (h : x H) :
              y * x H y H
              theorem add_mem_cancel_left {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] {x : G} {y : G} (h : x H) :
              x + y H y H
              theorem mul_mem_cancel_left {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] {x : G} {y : G} (h : x H) :
              x * y H y H
              instance NegMemClass.neg {G : Type u_1} {S : Type u_2} [Neg G] [SetLike S G] [NegMemClass S G] {H : S} :
              Neg { x : G // x H }

              An additive subgroup of an AddGroup inherits an inverse.

              Equations
              • NegMemClass.neg = { neg := fun (a : { x : G // x H }) => -a, }
              theorem NegMemClass.neg.proof_1 {G : Type u_1} {S : Type u_2} [Neg G] [SetLike S G] [NegMemClass S G] {H : S} (a : { x : G // x H }) :
              -a H
              instance InvMemClass.inv {G : Type u_1} {S : Type u_2} [Inv G] [SetLike S G] [InvMemClass S G] {H : S} :
              Inv { x : G // x H }

              A subgroup of a group inherits an inverse.

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

              Alias of InvMemClass.coe_inv.

              @[deprecated]
              theorem AddSubgroupClass.coe_neg {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : { x : G // x H }) :
              (-x) = -x
              theorem AddSubgroupClass.subset_union {G : Type u_1} [AddGroup G] {S : Type u_6} [SetLike S G] [AddSubgroupClass S G] {H : S} {K : S} {L : S} :
              H K L H K H L
              theorem SubgroupClass.subset_union {G : Type u_1} [Group G] {S : Type u_6} [SetLike S G] [SubgroupClass S G] {H : S} {K : S} {L : S} :
              H K L H K H L
              theorem AddSubgroupClass.sub.proof_1 {G : Type u_1} {S : Type u_2} [SubNegMonoid G] [SetLike S G] [AddSubgroupClass S G] {H : S} (a : { x : G // x H }) (b : { x : G // x H }) :
              a - b H
              instance AddSubgroupClass.sub {G : Type u_1} {S : Type u_2} [SubNegMonoid G] [SetLike S G] [AddSubgroupClass S G] {H : S} :
              Sub { x : G // x H }

              An additive subgroup of an AddGroup inherits a subtraction.

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

              A subgroup of a group inherits a division

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

              An additive subgroup of an AddGroup inherits an integer scaling.

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

              A subgroup of a group inherits an integer power.

              Equations
              • SubgroupClass.zpow = { pow := fun (a : { x : M // x H }) (n : ) => a ^ n, }
              @[simp]
              theorem AddSubgroupClass.coe_sub {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : { x : G // x H }) (y : { x : G // x H }) :
              (x - y) = x - y
              @[simp]
              theorem SubgroupClass.coe_div {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] (x : { x : G // x H }) (y : { x : G // x H }) :
              (x / y) = x / y
              theorem AddSubgroupClass.toAddGroup.proof_7 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
              ∀ (x : { x : G // x H }), (-x) = (-x)
              @[instance 75]
              instance AddSubgroupClass.toAddGroup {G : Type u_1} [AddGroup G] {S : Type u_6} (H : S) [SetLike S G] [AddSubgroupClass S G] :
              AddGroup { x : G // x H }

              An additive subgroup of an AddGroup inherits an AddGroup structure.

              Equations
              theorem AddSubgroupClass.toAddGroup.proof_6 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
              ∀ (x x_1 : { x : G // x H }), (x + x_1) = (x + x_1)
              theorem AddSubgroupClass.toAddGroup.proof_8 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
              ∀ (x x_1 : { x : G // x H }), (x - x_1) = (x - x_1)
              theorem AddSubgroupClass.toAddGroup.proof_5 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
              0 = 0
              theorem AddSubgroupClass.toAddGroup.proof_9 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
              ∀ (x : { x : G // x H }) (x_1 : ), (x_1 x) = (x_1 x)
              theorem AddSubgroupClass.toAddGroup.proof_10 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
              ∀ (x : { x : G // x H }) (x_1 : ), (x_1 x) = (x_1 x)
              theorem AddSubgroupClass.toAddGroup.proof_4 {G : Type u_1} {S : Type u_2} (H : S) [SetLike S G] :
              Function.Injective fun (a : { x : G // x H }) => a
              @[instance 75]
              instance SubgroupClass.toGroup {G : Type u_1} [Group G] {S : Type u_6} (H : S) [SetLike S G] [SubgroupClass S G] :
              Group { x : G // x H }

              A subgroup of a group inherits a group structure.

              Equations
              theorem AddSubgroupClass.toAddCommGroup.proof_9 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
              ∀ (x : { x : G // x H }) (x_1 : ), (x_1 x) = (x_1 x)
              theorem AddSubgroupClass.toAddCommGroup.proof_8 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
              ∀ (x x_1 : { x : G // x H }), (x - x_1) = (x - x_1)
              theorem AddSubgroupClass.toAddCommGroup.proof_10 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
              ∀ (x : { x : G // x H }) (x_1 : ), (x_1 x) = (x_1 x)
              theorem AddSubgroupClass.toAddCommGroup.proof_7 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
              ∀ (x : { x : G // x H }), (-x) = (-x)
              @[instance 75]
              instance AddSubgroupClass.toAddCommGroup {S : Type u_6} (H : S) {G : Type u_7} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
              AddCommGroup { x : G // x H }

              An additive subgroup of an AddCommGroup is an AddCommGroup.

              Equations
              theorem AddSubgroupClass.toAddCommGroup.proof_4 {S : Type u_2} (H : S) {G : Type u_1} [SetLike S G] :
              Function.Injective fun (a : { x : G // x H }) => a
              theorem AddSubgroupClass.toAddCommGroup.proof_6 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
              ∀ (x x_1 : { x : G // x H }), (x + x_1) = (x + x_1)
              theorem AddSubgroupClass.toAddCommGroup.proof_5 {S : Type u_2} (H : S) {G : Type u_1} [AddCommGroup G] [SetLike S G] [AddSubgroupClass S G] :
              0 = 0
              @[instance 75]
              instance SubgroupClass.toCommGroup {S : Type u_6} (H : S) {G : Type u_7} [CommGroup G] [SetLike S G] [SubgroupClass S G] :
              CommGroup { x : G // x H }

              A subgroup of a CommGroup is a CommGroup.

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

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

              Equations
              • H = { toFun := Subtype.val, map_zero' := , map_add' := }
              Instances For
                theorem AddSubgroupClass.subtype.proof_1 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                0 = 0
                theorem AddSubgroupClass.subtype.proof_2 {G : Type u_1} [AddGroup G] {S : Type u_2} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                ∀ (x x_1 : { x : G // x H }), { toFun := Subtype.val, map_zero' := }.toFun (x + x_1) = { toFun := Subtype.val, map_zero' := }.toFun (x + x_1)
                def SubgroupClass.subtype {G : Type u_1} [Group G] {S : Type u_6} (H : S) [SetLike S G] [SubgroupClass S G] :
                { x : G // x H } →* G

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

                Equations
                • H = { toFun := Subtype.val, map_one' := , map_mul' := }
                Instances For
                  @[simp]
                  theorem AddSubgroupClass.coeSubtype {G : Type u_1} [AddGroup G] {S : Type u_6} (H : S) [SetLike S G] [AddSubgroupClass S G] :
                  H = Subtype.val
                  @[simp]
                  theorem SubgroupClass.coeSubtype {G : Type u_1} [Group G] {S : Type u_6} (H : S) [SetLike S G] [SubgroupClass S G] :
                  H = Subtype.val
                  @[simp]
                  theorem AddSubgroupClass.coe_nsmul {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : { x : G // x H }) (n : ) :
                  (n x) = n x
                  @[simp]
                  theorem SubgroupClass.coe_pow {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] (x : { x : G // x H }) (n : ) :
                  (x ^ n) = x ^ n
                  @[simp]
                  theorem AddSubgroupClass.coe_zsmul {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] (x : { x : G // x H }) (n : ) :
                  (n x) = n x
                  @[simp]
                  theorem SubgroupClass.coe_zpow {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] (x : { x : G // x H }) (n : ) :
                  (x ^ n) = x ^ n
                  theorem AddSubgroupClass.inclusion.proof_2 {G : Type u_1} [AddGroup G] {S : Type u_2} [SetLike S G] [AddSubgroupClass S G] {H : S} {K : S} (h : H K) :
                  ∀ (x x_1 : { x : G // x H }), (fun (x : { x : G // x H }) => x, ) (x + x_1) = (fun (x : { x : G // x H }) => x, ) (x + x_1)
                  theorem AddSubgroupClass.inclusion.proof_1 {G : Type u_1} {S : Type u_2} [SetLike S G] {H : S} {K : S} (h : H K) (x : { x : G // x H }) :
                  x K
                  def AddSubgroupClass.inclusion {G : Type u_1} [AddGroup G] {S : Type u_6} [SetLike S G] [AddSubgroupClass S G] {H : S} {K : S} (h : H K) :
                  { x : G // x H } →+ { x : G // x K }

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

                  Equations
                  Instances For
                    def SubgroupClass.inclusion {G : Type u_1} [Group G] {S : Type u_6} [SetLike S G] [SubgroupClass S G] {H : S} {K : S} (h : H K) :
                    { x : G // x H } →* { x : G // x K }

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

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

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

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

                        G is closed under inverses

                      Instances For
                        theorem Subgroup.inv_mem' {G : Type u_5} [Group G] (self : Subgroup G) {x : G} :
                        x self.carrierx⁻¹ self.carrier

                        G is closed under inverses

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

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

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

                          G is closed under negation

                        Instances For
                          theorem AddSubgroup.neg_mem' {G : Type u_5} [AddGroup G] (self : AddSubgroup G) {x : G} :
                          x self.carrier-x self.carrier

                          G is closed under negation

                          theorem AddSubgroup.instSetLike.proof_1 {G : Type u_1} [AddGroup G] (p : AddSubgroup G) (q : AddSubgroup G) (h : (fun (s : AddSubgroup G) => s.carrier) p = (fun (s : AddSubgroup G) => s.carrier) q) :
                          p = q
                          Equations
                          • AddSubgroup.instSetLike = { coe := fun (s : AddSubgroup G) => s.carrier, coe_injective' := }
                          instance Subgroup.instSetLike {G : Type u_1} [Group G] :
                          Equations
                          • Subgroup.instSetLike = { coe := fun (s : Subgroup G) => s.carrier, coe_injective' := }
                          Equations
                          • =
                          @[simp]
                          theorem AddSubgroup.mem_carrier {G : Type u_1} [AddGroup G] {s : AddSubgroup G} {x : G} :
                          x s.carrier x s
                          @[simp]
                          theorem Subgroup.mem_carrier {G : Type u_1} [Group G] {s : Subgroup G} {x : G} :
                          x s.carrier x s
                          @[simp]
                          theorem AddSubgroup.mem_mk {G : Type u_1} [AddGroup G] {s : Set G} {x : G} (h_one : ∀ {a b : G}, a sb sa + b s) (h_mul : s 0) (h_inv : ∀ {x : G}, x { 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.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.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.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.mk_le_mk {G : Type u_1} [AddGroup G] {s : Set G} {t : Set G} (h_one : ∀ {a b : G}, a sb sa + b s) (h_mul : s 0) (h_inv : ∀ {x : G}, x { 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.mk_le_mk {G : Type u_1} [Group G] {s : Set G} {t : Set G} (h_one : ∀ {a b : G}, a sb sa * b s) (h_mul : s 1) (h_inv : ∀ {x : G}, x { 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.coe_toAddSubmonoid {G : Type u_1} [AddGroup G] (K : AddSubgroup G) :
                          K.toAddSubmonoid = K
                          @[simp]
                          theorem Subgroup.coe_toSubmonoid {G : Type u_1} [Group G] (K : Subgroup G) :
                          K.toSubmonoid = K
                          @[simp]
                          theorem AddSubgroup.mem_toAddSubmonoid {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (x : G) :
                          x K.toAddSubmonoid x K
                          @[simp]
                          theorem Subgroup.mem_toSubmonoid {G : Type u_1} [Group G] (K : Subgroup G) (x : G) :
                          x K.toSubmonoid x K
                          theorem AddSubgroup.toAddSubmonoid_injective {G : Type u_1} [AddGroup G] :
                          Function.Injective AddSubgroup.toAddSubmonoid
                          theorem Subgroup.toSubmonoid_injective {G : Type u_1} [Group G] :
                          Function.Injective Subgroup.toSubmonoid
                          @[simp]
                          theorem AddSubgroup.toAddSubmonoid_eq {G : Type u_1} [AddGroup G] {p : AddSubgroup G} {q : AddSubgroup G} :
                          p.toAddSubmonoid = q.toAddSubmonoid p = q
                          @[simp]
                          theorem Subgroup.toSubmonoid_eq {G : Type u_1} [Group G] {p : Subgroup G} {q : Subgroup G} :
                          p.toSubmonoid = q.toSubmonoid p = q
                          theorem AddSubgroup.toAddSubmonoid_strictMono {G : Type u_1} [AddGroup G] :
                          StrictMono AddSubgroup.toAddSubmonoid
                          theorem Subgroup.toSubmonoid_strictMono {G : Type u_1} [Group G] :
                          StrictMono Subgroup.toSubmonoid
                          theorem AddSubgroup.toAddSubmonoid_mono {G : Type u_1} [AddGroup G] :
                          Monotone AddSubgroup.toAddSubmonoid
                          theorem Subgroup.toSubmonoid_mono {G : Type u_1} [Group G] :
                          Monotone Subgroup.toSubmonoid
                          @[simp]
                          theorem AddSubgroup.toAddSubmonoid_le {G : Type u_1} [AddGroup G] {p : AddSubgroup G} {q : AddSubgroup G} :
                          p.toAddSubmonoid q.toAddSubmonoid p q
                          @[simp]
                          theorem Subgroup.toSubmonoid_le {G : Type u_1} [Group G] {p : Subgroup G} {q : Subgroup G} :
                          p.toSubmonoid q.toSubmonoid p q
                          @[simp]
                          theorem AddSubgroup.coe_nonempty {G : Type u_1} [AddGroup G] (s : AddSubgroup G) :
                          (↑s).Nonempty
                          @[simp]
                          theorem Subgroup.coe_nonempty {G : Type u_1} [Group G] (s : Subgroup G) :
                          (↑s).Nonempty

                          Conversion to/from Additive/Multiplicative #

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

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[reducible, inline]

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

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

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

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[reducible, inline]

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

                                Equations
                                • Subgroup.toAddSubgroup' = AddSubgroup.toSubgroup.symm
                                Instances For
                                  theorem AddSubgroup.copy.proof_2 {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :
                                  0 { carrier := s, add_mem' := }.carrier
                                  theorem AddSubgroup.copy.proof_3 {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :
                                  ∀ {x : G}, x { carrier := s, add_mem' := , zero_mem' := }.carrier-x { carrier := s, add_mem' := , zero_mem' := }.carrier
                                  theorem AddSubgroup.copy.proof_1 {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :
                                  ∀ {a b : G}, a sb sa + b s
                                  def AddSubgroup.copy {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = K) :

                                  Copy of an additive subgroup with a new carrier equal to the old one. Useful to fix definitional equalities

                                  Equations
                                  • K.copy s hs = { carrier := s, add_mem' := , zero_mem' := , neg_mem' := }
                                  Instances For
                                    def Subgroup.copy {G : Type u_1} [Group G] (K : Subgroup G) (s : Set G) (hs : s = K) :

                                    Copy of a subgroup with a new carrier equal to the old one. Useful to fix definitional equalities.

                                    Equations
                                    • K.copy s hs = { carrier := s, mul_mem' := , one_mem' := , inv_mem' := }
                                    Instances For
                                      @[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
                                      @[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
                                      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.copy_eq {G : Type u_1} [Group G] (K : Subgroup G) (s : Set G) (hs : s = K) :
                                      K.copy s hs = K
                                      theorem AddSubgroup.ext {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : ∀ (x : G), x H x K) :
                                      H = K

                                      Two AddSubgroups are equal if they have the same elements.

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

                                      Two subgroups are equal if they have the same elements.

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

                                      An AddSubgroup contains the group's 0.

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

                                      A subgroup contains the group's 1.

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

                                      An AddSubgroup is closed under addition.

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

                                      A subgroup is closed under multiplication.

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

                                      An AddSubgroup is closed under inverse.

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

                                      A subgroup is closed under inverse.

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

                                      An AddSubgroup is closed under subtraction.

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

                                      A subgroup is closed under division.

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

                                          An AddSubgroup of an AddGroup inherits an addition.

                                          Equations
                                          • H.add = H.add
                                          instance Subgroup.mul {G : Type u_1} [Group G] (H : Subgroup G) :
                                          Mul { x : G // x H }

                                          A subgroup of a group inherits a multiplication.

                                          Equations
                                          • H.mul = H.mul
                                          instance AddSubgroup.zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          Zero { x : G // x H }

                                          An AddSubgroup of an AddGroup inherits a zero.

                                          Equations
                                          • H.zero = H.zero
                                          instance Subgroup.one {G : Type u_1} [Group G] (H : Subgroup G) :
                                          One { x : G // x H }

                                          A subgroup of a group inherits a 1.

                                          Equations
                                          • H.one = H.one
                                          instance AddSubgroup.neg {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          Neg { x : G // x H }

                                          An AddSubgroup of an AddGroup inherits an inverse.

                                          Equations
                                          • H.neg = { neg := fun (a : { x : G // x H }) => -a, }
                                          theorem AddSubgroup.neg.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (a : { x : G // x H }) :
                                          -a H
                                          instance Subgroup.inv {G : Type u_1} [Group G] (H : Subgroup G) :
                                          Inv { x : G // x H }

                                          A subgroup of a group inherits an inverse.

                                          Equations
                                          • H.inv = { inv := fun (a : { x : G // x H }) => (↑a)⁻¹, }
                                          theorem AddSubgroup.sub.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (a : { x : G // x H }) (b : { x : G // x H }) :
                                          a - b H
                                          instance AddSubgroup.sub {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          Sub { x : G // x H }

                                          An AddSubgroup of an AddGroup inherits a subtraction.

                                          Equations
                                          • H.sub = { sub := fun (a b : { x : G // x H }) => a - b, }
                                          instance Subgroup.div {G : Type u_1} [Group G] (H : Subgroup G) :
                                          Div { x : G // x H }

                                          A subgroup of a group inherits a division

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

                                          An AddSubgroup of an AddGroup inherits a natural scaling.

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

                                          A subgroup of a group inherits a natural power

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

                                          An AddSubgroup of an AddGroup inherits an integer scaling.

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

                                          A subgroup of a group inherits an integer power

                                          Equations
                                          • H.zpow = { pow := fun (a : { x : G // x H }) (n : ) => a ^ n, }
                                          @[simp]
                                          theorem AddSubgroup.coe_add {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : { x : G // x H }) (y : { x : G // x H }) :
                                          (x + y) = x + y
                                          @[simp]
                                          theorem Subgroup.coe_mul {G : Type u_1} [Group G] (H : Subgroup G) (x : { x : G // x H }) (y : { x : G // x H }) :
                                          (x * y) = x * y
                                          @[simp]
                                          theorem AddSubgroup.coe_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          0 = 0
                                          @[simp]
                                          theorem Subgroup.coe_one {G : Type u_1} [Group G] (H : Subgroup G) :
                                          1 = 1
                                          @[simp]
                                          theorem AddSubgroup.coe_neg {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : { x : G // x H }) :
                                          (-x) = -x
                                          @[simp]
                                          theorem Subgroup.coe_inv {G : Type u_1} [Group G] (H : Subgroup G) (x : { x : G // x H }) :
                                          x⁻¹ = (↑x)⁻¹
                                          @[simp]
                                          theorem AddSubgroup.coe_sub {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : { x : G // x H }) (y : { x : G // x H }) :
                                          (x - y) = x - y
                                          @[simp]
                                          theorem Subgroup.coe_div {G : Type u_1} [Group G] (H : Subgroup G) (x : { x : G // x H }) (y : { x : G // x H }) :
                                          (x / y) = x / y
                                          theorem AddSubgroup.coe_mk {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : G) (hx : x H) :
                                          x, hx = x
                                          theorem Subgroup.coe_mk {G : Type u_1} [Group G] (H : Subgroup G) (x : G) (hx : x H) :
                                          x, hx = x
                                          @[simp]
                                          theorem AddSubgroup.coe_nsmul {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : { x : G // x H }) (n : ) :
                                          (n x) = n x
                                          @[simp]
                                          theorem Subgroup.coe_pow {G : Type u_1} [Group G] (H : Subgroup G) (x : { x : G // x H }) (n : ) :
                                          (x ^ n) = x ^ n
                                          theorem AddSubgroup.coe_zsmul {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (x : { x : G // x H }) (n : ) :
                                          (n x) = n x
                                          theorem Subgroup.coe_zpow {G : Type u_1} [Group G] (H : Subgroup G) (x : { x : G // x H }) (n : ) :
                                          (x ^ n) = x ^ n
                                          @[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
                                          @[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
                                          theorem AddSubgroup.toAddGroup.proof_5 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          ∀ (x x_1 : { x : G // x H }), (x - x_1) = (x - x_1)
                                          instance AddSubgroup.toAddGroup {G : Type u_5} [AddGroup G] (H : AddSubgroup G) :
                                          AddGroup { x : G // x H }

                                          An AddSubgroup of an AddGroup inherits an AddGroup structure.

                                          Equations
                                          theorem AddSubgroup.toAddGroup.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          Function.Injective fun (a : { x : G // x H }) => a
                                          theorem AddSubgroup.toAddGroup.proof_7 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          ∀ (x : { x : G // x H }) (x_1 : ), (x_1 x) = (x_1 x)
                                          theorem AddSubgroup.toAddGroup.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          0 = 0
                                          theorem AddSubgroup.toAddGroup.proof_6 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          ∀ (x : { x : G // x H }) (x_1 : ), (x_1 x) = (x_1 x)
                                          theorem AddSubgroup.toAddGroup.proof_3 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          ∀ (x x_1 : { x : G // x H }), (x + x_1) = (x + x_1)
                                          theorem AddSubgroup.toAddGroup.proof_4 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          ∀ (x : { x : G // x H }), (-x) = (-x)
                                          instance Subgroup.toGroup {G : Type u_5} [Group G] (H : Subgroup G) :
                                          Group { x : G // x H }

                                          A subgroup of a group inherits a group structure.

                                          Equations
                                          theorem AddSubgroup.toAddCommGroup.proof_5 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) :
                                          ∀ (x x_1 : { x : G // x H }), (x - x_1) = (x - x_1)
                                          theorem AddSubgroup.toAddCommGroup.proof_6 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) :
                                          ∀ (x : { x : G // x H }) (x_1 : ), (x_1 x) = (x_1 x)
                                          theorem AddSubgroup.toAddCommGroup.proof_4 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) :
                                          ∀ (x : { x : G // x H }), (-x) = (-x)
                                          theorem AddSubgroup.toAddCommGroup.proof_7 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) :
                                          ∀ (x : { x : G // x H }) (x_1 : ), (x_1 x) = (x_1 x)
                                          theorem AddSubgroup.toAddCommGroup.proof_3 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) :
                                          ∀ (x x_1 : { x : G // x H }), (x + x_1) = (x + x_1)
                                          theorem AddSubgroup.toAddCommGroup.proof_1 {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) :
                                          Function.Injective fun (a : { x : G // x H }) => a
                                          instance AddSubgroup.toAddCommGroup {G : Type u_5} [AddCommGroup G] (H : AddSubgroup G) :
                                          AddCommGroup { x : G // x H }

                                          An AddSubgroup of an AddCommGroup is an AddCommGroup.

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

                                          A subgroup of a CommGroup is a CommGroup.

                                          Equations
                                          theorem AddSubgroup.subtype.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          ∀ (x x_1 : { x : G // x H }), { toFun := Subtype.val, map_zero' := }.toFun (x + x_1) = { toFun := Subtype.val, map_zero' := }.toFun (x + x_1)
                                          theorem AddSubgroup.subtype.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          0 = 0
                                          def AddSubgroup.subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                          { x : G // x H } →+ G

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

                                          Equations
                                          • H.subtype = { toFun := Subtype.val, map_zero' := , map_add' := }
                                          Instances For
                                            def Subgroup.subtype {G : Type u_1} [Group G] (H : Subgroup G) :
                                            { x : G // x H } →* G

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

                                            Equations
                                            • H.subtype = { toFun := Subtype.val, map_one' := , map_mul' := }
                                            Instances For
                                              @[simp]
                                              theorem AddSubgroup.coeSubtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                              H.subtype = Subtype.val
                                              @[simp]
                                              theorem Subgroup.coeSubtype {G : Type u_1} [Group G] (H : Subgroup G) :
                                              H.subtype = Subtype.val
                                              theorem Subgroup.subtype_injective {G : Type u_1} [Group G] (H : Subgroup G) :
                                              Function.Injective H.subtype
                                              theorem AddSubgroup.inclusion.proof_2 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) :
                                              ∀ (x x_1 : { x : G // x H }), (fun (x : { x : G // x H }) => x, ) (x + x_1) = (fun (x : { x : G // x H }) => x, ) (x + x_1)
                                              def AddSubgroup.inclusion {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) :
                                              { x : G // x H } →+ { x : G // x K }

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

                                              Equations
                                              Instances For
                                                theorem AddSubgroup.inclusion.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) (x : { x : G // x H }) :
                                                x K
                                                def Subgroup.inclusion {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H K) :
                                                { x : G // x H } →* { x : G // x K }

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

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

                                                  The AddSubgroup G of the AddGroup G.

                                                  Equations
                                                  • AddSubgroup.instTop = { top := let __src := ; { toAddSubmonoid := __src, neg_mem' := } }
                                                  theorem AddSubgroup.instTop.proof_1 {G : Type u_1} [AddGroup G] :
                                                  ∀ {x : G}, x .carrier-x Set.univ
                                                  instance Subgroup.instTop {G : Type u_1} [Group G] :

                                                  The subgroup G of the group G.

                                                  Equations
                                                  • Subgroup.instTop = { top := let __src := ; { toSubmonoid := __src, inv_mem' := } }
                                                  def AddSubgroup.topEquiv {G : Type u_1} [AddGroup G] :
                                                  { x : G // x } ≃+ G

                                                  The top additive subgroup is isomorphic to the additive group.

                                                  This is the additive group version of AddSubmonoid.topEquiv.

                                                  Equations
                                                  • AddSubgroup.topEquiv = AddSubmonoid.topEquiv
                                                  Instances For
                                                    @[simp]
                                                    theorem Subgroup.topEquiv_symm_apply_coe {G : Type u_1} [Group G] (x : G) :
                                                    (Subgroup.topEquiv.symm x) = x
                                                    @[simp]
                                                    theorem AddSubgroup.topEquiv_apply {G : Type u_1} [AddGroup G] (x : { x : G // x }) :
                                                    AddSubgroup.topEquiv x = x
                                                    @[simp]
                                                    theorem AddSubgroup.topEquiv_symm_apply_coe {G : Type u_1} [AddGroup G] (x : G) :
                                                    (AddSubgroup.topEquiv.symm x) = x
                                                    @[simp]
                                                    theorem Subgroup.topEquiv_apply {G : Type u_1} [Group G] (x : { x : G // x }) :
                                                    Subgroup.topEquiv x = x
                                                    def Subgroup.topEquiv {G : Type u_1} [Group G] :
                                                    { x : G // x } ≃* G

                                                    The top subgroup is isomorphic to the group.

                                                    This is the group version of Submonoid.topEquiv.

                                                    Equations
                                                    • Subgroup.topEquiv = Submonoid.topEquiv
                                                    Instances For
                                                      theorem AddSubgroup.instBot.proof_1 {G : Type u_1} [AddGroup G] (a : G) :
                                                      a .carrier-a .carrier
                                                      instance AddSubgroup.instBot {G : Type u_1} [AddGroup G] :

                                                      The trivial AddSubgroup {0} of an AddGroup G.

                                                      Equations
                                                      • AddSubgroup.instBot = { bot := let __src := ; { toAddSubmonoid := __src, neg_mem' := } }
                                                      instance Subgroup.instBot {G : Type u_1} [Group G] :

                                                      The trivial subgroup {1} of a group G.

                                                      Equations
                                                      • Subgroup.instBot = { bot := let __src := ; { toSubmonoid := __src, inv_mem' := } }
                                                      Equations
                                                      • AddSubgroup.instInhabited = { default := }
                                                      instance Subgroup.instInhabited {G : Type u_1} [Group G] :
                                                      Equations
                                                      • Subgroup.instInhabited = { default := }
                                                      @[simp]
                                                      theorem AddSubgroup.mem_bot {G : Type u_1} [AddGroup G] {x : G} :
                                                      x x = 0
                                                      @[simp]
                                                      theorem Subgroup.mem_bot {G : Type u_1} [Group G] {x : G} :
                                                      x x = 1
                                                      @[simp]
                                                      theorem AddSubgroup.mem_top {G : Type u_1} [AddGroup G] (x : G) :
                                                      @[simp]
                                                      theorem Subgroup.mem_top {G : Type u_1} [Group G] (x : G) :
                                                      @[simp]
                                                      theorem AddSubgroup.coe_top {G : Type u_1} [AddGroup G] :
                                                      = Set.univ
                                                      @[simp]
                                                      theorem Subgroup.coe_top {G : Type u_1} [Group G] :
                                                      = Set.univ
                                                      @[simp]
                                                      theorem AddSubgroup.coe_bot {G : Type u_1} [AddGroup G] :
                                                      = {0}
                                                      @[simp]
                                                      theorem Subgroup.coe_bot {G : Type u_1} [Group G] :
                                                      = {1}
                                                      instance AddSubgroup.instUniqueSubtypeMemBot {G : Type u_1} [AddGroup G] :
                                                      Unique { x : G // x }
                                                      Equations
                                                      • AddSubgroup.instUniqueSubtypeMemBot = { default := 0, uniq := }
                                                      theorem AddSubgroup.instUniqueSubtypeMemBot.proof_1 {G : Type u_1} [AddGroup G] (g : { x : G // x }) :
                                                      g = default
                                                      instance Subgroup.instUniqueSubtypeMemBot {G : Type u_1} [Group G] :
                                                      Unique { x : G // x }
                                                      Equations
                                                      • Subgroup.instUniqueSubtypeMemBot = { default := 1, uniq := }
                                                      @[simp]
                                                      theorem AddSubgroup.top_toAddSubmonoid {G : Type u_1} [AddGroup G] :
                                                      .toAddSubmonoid =
                                                      @[simp]
                                                      theorem Subgroup.top_toSubmonoid {G : Type u_1} [Group G] :
                                                      .toSubmonoid =
                                                      @[simp]
                                                      theorem AddSubgroup.bot_toAddSubmonoid {G : Type u_1} [AddGroup G] :
                                                      .toAddSubmonoid =
                                                      @[simp]
                                                      theorem Subgroup.bot_toSubmonoid {G : Type u_1} [Group G] :
                                                      .toSubmonoid =
                                                      theorem AddSubgroup.eq_bot_iff_forall {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                      H = xH, x = 0
                                                      theorem Subgroup.eq_bot_iff_forall {G : Type u_1} [Group G] (H : Subgroup G) :
                                                      H = xH, x = 1
                                                      theorem AddSubgroup.eq_bot_of_subsingleton {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Subsingleton { x : G // x H }] :
                                                      H =
                                                      theorem Subgroup.eq_bot_of_subsingleton {G : Type u_1} [Group G] (H : Subgroup G) [Subsingleton { x : G // x H }] :
                                                      H =
                                                      @[simp]
                                                      theorem AddSubgroup.coe_eq_univ {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                      H = Set.univ H =
                                                      @[simp]
                                                      theorem Subgroup.coe_eq_univ {G : Type u_1} [Group G] {H : Subgroup G} :
                                                      H = Set.univ H =
                                                      theorem AddSubgroup.coe_eq_singleton {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                      (∃ (g : G), H = {g}) H =
                                                      theorem Subgroup.coe_eq_singleton {G : Type u_1} [Group G] {H : Subgroup G} :
                                                      (∃ (g : G), H = {g}) H =
                                                      theorem AddSubgroup.nontrivial_iff_exists_ne_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                      Nontrivial { x : G // x H } xH, x 0
                                                      theorem Subgroup.nontrivial_iff_exists_ne_one {G : Type u_1} [Group G] (H : Subgroup G) :
                                                      Nontrivial { x : G // x H } xH, x 1
                                                      theorem AddSubgroup.exists_ne_zero_of_nontrivial {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Nontrivial { x : G // x H }] :
                                                      xH, x 0
                                                      theorem Subgroup.exists_ne_one_of_nontrivial {G : Type u_1} [Group G] (H : Subgroup G) [Nontrivial { x : G // x H }] :
                                                      xH, x 1
                                                      theorem AddSubgroup.nontrivial_iff_ne_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                      Nontrivial { x : G // x H } H
                                                      theorem Subgroup.nontrivial_iff_ne_bot {G : Type u_1} [Group G] (H : Subgroup G) :
                                                      Nontrivial { x : G // x H } H
                                                      theorem AddSubgroup.bot_or_nontrivial {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                      H = Nontrivial { x : G // x H }

                                                      A subgroup is either the trivial subgroup or nontrivial.

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

                                                      A subgroup is either the trivial subgroup or nontrivial.

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

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

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

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

                                                      theorem AddSubgroup.ne_bot_iff_exists_ne_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                      H ∃ (a : { x : G // x H }), a 0
                                                      theorem Subgroup.ne_bot_iff_exists_ne_one {G : Type u_1} [Group G] {H : Subgroup G} :
                                                      H ∃ (a : { x : G // x H }), a 1
                                                      theorem AddSubgroup.instInf.proof_1 {G : Type u_1} [AddGroup G] (H₁ : AddSubgroup G) (H₂ : AddSubgroup G) :
                                                      ∀ {x : G}, x (H₁.toAddSubmonoid H₂.toAddSubmonoid).carrier-x (H₁.toAddSubmonoid H₂.toAddSubmonoid).carrier
                                                      instance AddSubgroup.instInf {G : Type u_1} [AddGroup G] :

                                                      The inf of two AddSubgroups is their intersection.

                                                      Equations
                                                      • AddSubgroup.instInf = { inf := fun (H₁ H₂ : AddSubgroup G) => let __src := H₁.toAddSubmonoid H₂.toAddSubmonoid; { toAddSubmonoid := __src, neg_mem' := } }
                                                      instance Subgroup.instInf {G : Type u_1} [Group G] :

                                                      The inf of two subgroups is their intersection.

                                                      Equations
                                                      • Subgroup.instInf = { inf := fun (H₁ H₂ : Subgroup G) => let __src := H₁.toSubmonoid H₂.toSubmonoid; { toSubmonoid := __src, inv_mem' := } }
                                                      @[simp]
                                                      theorem AddSubgroup.coe_inf {G : Type u_1} [AddGroup G] (p : AddSubgroup G) (p' : AddSubgroup G) :
                                                      (p p') = p p'
                                                      @[simp]
                                                      theorem Subgroup.coe_inf {G : Type u_1} [Group G] (p : Subgroup G) (p' : Subgroup G) :
                                                      (p p') = p p'
                                                      @[simp]
                                                      theorem AddSubgroup.mem_inf {G : Type u_1} [AddGroup G] {p : AddSubgroup G} {p' : AddSubgroup G} {x : G} :
                                                      x p p' x p x p'
                                                      @[simp]
                                                      theorem Subgroup.mem_inf {G : Type u_1} [Group G] {p : Subgroup G} {p' : Subgroup G} {x : G} :
                                                      x p p' x p x p'
                                                      Equations
                                                      • AddSubgroup.instInfSet = { sInf := fun (s : Set (AddSubgroup G)) => let __src := (⨅ Ss, S.toAddSubmonoid).copy (⋂ Ss, S) ; { toAddSubmonoid := __src, neg_mem' := } }
                                                      theorem AddSubgroup.instInfSet.proof_2 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) {x : G} (hx : x ((⨅ Ss, S.toAddSubmonoid).copy (⋂ Ss, S) ).carrier) :
                                                      -x xs, x
                                                      theorem AddSubgroup.instInfSet.proof_1 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) :
                                                      Ss, S = (⨅ is, i.toAddSubmonoid)
                                                      instance Subgroup.instInfSet {G : Type u_1} [Group G] :
                                                      Equations
                                                      • Subgroup.instInfSet = { sInf := fun (s : Set (Subgroup G)) => let __src := (⨅ Ss, S.toSubmonoid).copy (⋂ Ss, S) ; { toSubmonoid := __src, inv_mem' := } }
                                                      @[simp]
                                                      theorem AddSubgroup.coe_sInf {G : Type u_1} [AddGroup G] (H : Set (AddSubgroup G)) :
                                                      (sInf H) = sH, s
                                                      @[simp]
                                                      theorem Subgroup.coe_sInf {G : Type u_1} [Group G] (H : Set (Subgroup G)) :
                                                      (sInf H) = sH, s
                                                      @[simp]
                                                      theorem AddSubgroup.mem_sInf {G : Type u_1} [AddGroup G] {S : Set (AddSubgroup G)} {x : G} :
                                                      x sInf S pS, x p
                                                      @[simp]
                                                      theorem Subgroup.mem_sInf {G : Type u_1} [Group G] {S : Set (Subgroup G)} {x : G} :
                                                      x sInf S pS, x p
                                                      theorem AddSubgroup.mem_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_5} {S : ιAddSubgroup G} {x : G} :
                                                      x ⨅ (i : ι), S i ∀ (i : ι), x S i
                                                      theorem Subgroup.mem_iInf {G : Type u_1} [Group G] {ι : Sort u_5} {S : ιSubgroup G} {x : G} :
                                                      x ⨅ (i : ι), S i ∀ (i : ι), x S i
                                                      @[simp]
                                                      theorem AddSubgroup.coe_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_5} {S : ιAddSubgroup G} :
                                                      (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
                                                      @[simp]
                                                      theorem Subgroup.coe_iInf {G : Type u_1} [Group G] {ι : Sort u_5} {S : ιSubgroup G} :
                                                      (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)

                                                      The AddSubgroups of an AddGroup form a complete lattice.

                                                      Equations
                                                      theorem AddSubgroup.instCompleteLattice.proof_9 {G : Type u_1} [AddGroup G] (S : AddSubgroup G) (_x : G) (hx : _x ) :
                                                      _x S
                                                      theorem AddSubgroup.instCompleteLattice.proof_2 {G : Type u_1} [AddGroup G] (_a : AddSubgroup G) (_b : AddSubgroup G) (_x : G) (self : _x _a.toAddSubmonoid _x _b.toAddSubmonoid) :
                                                      _x _a.toAddSubmonoid
                                                      theorem AddSubgroup.instCompleteLattice.proof_8 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) :
                                                      (∀ bs, a b)a sInf s
                                                      theorem AddSubgroup.instCompleteLattice.proof_4 {G : Type u_1} [AddGroup G] (_a : AddSubgroup G) (_b : AddSubgroup G) (_c : AddSubgroup G) (ha : _a _b) (hb : _a _c) (_x : G) (hx : _x _a) :
                                                      _x _b.toAddSubmonoid _x _c.toAddSubmonoid
                                                      theorem AddSubgroup.instCompleteLattice.proof_6 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) :
                                                      (∀ bs, b a)sSup s a
                                                      theorem AddSubgroup.instCompleteLattice.proof_3 {G : Type u_1} [AddGroup G] (_a : AddSubgroup G) (_b : AddSubgroup G) (_x : G) (self : _x _a.toAddSubmonoid _x _b.toAddSubmonoid) :
                                                      _x _b.toAddSubmonoid

                                                      Subgroups of a group form a complete lattice.

                                                      Equations
                                                      theorem AddSubgroup.mem_sup_left {G : Type u_1} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} {x : G} :
                                                      x Sx S T
                                                      theorem Subgroup.mem_sup_left {G : Type u_1} [Group G] {S : Subgroup G} {T : Subgroup G} {x : G} :
                                                      x Sx S T
                                                      theorem AddSubgroup.mem_sup_right {G : Type u_1} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} {x : G} :
                                                      x Tx S T
                                                      theorem Subgroup.mem_sup_right {G : Type u_1} [Group G] {S : Subgroup G} {T : Subgroup G} {x : G} :
                                                      x Tx S T
                                                      theorem AddSubgroup.add_mem_sup {G : Type u_1} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} {x : G} {y : G} (hx : x S) (hy : y T) :
                                                      x + y S T
                                                      theorem Subgroup.mul_mem_sup {G : Type u_1} [Group G] {S : Subgroup G} {T : Subgroup G} {x : G} {y : G} (hx : x S) (hy : y T) :
                                                      x * y S T
                                                      theorem AddSubgroup.mem_iSup_of_mem {G : Type u_1} [AddGroup G] {ι : Sort u_5} {S : ιAddSubgroup G} (i : ι) {x : G} :
                                                      x S ix iSup S
                                                      theorem Subgroup.mem_iSup_of_mem {G : Type u_1} [Group G] {ι : Sort u_5} {S : ιSubgroup G} (i : ι) {x : G} :
                                                      x S ix iSup S
                                                      theorem AddSubgroup.mem_sSup_of_mem {G : Type u_1} [AddGroup G] {S : Set (AddSubgroup G)} {s : AddSubgroup G} (hs : s S) {x : G} :
                                                      x sx sSup S
                                                      theorem Subgroup.mem_sSup_of_mem {G : Type u_1} [Group G] {S : Set (Subgroup G)} {s : Subgroup G} (hs : s S) {x : G} :
                                                      x sx sSup S
                                                      Equations
                                                      • AddSubgroup.instUniqueOfSubsingleton = { default := , uniq := }
                                                      Equations
                                                      • Subgroup.instUniqueOfSubsingleton = { default := , uniq := }
                                                      Equations
                                                      • =
                                                      Equations
                                                      • =
                                                      theorem AddSubgroup.eq_top_iff' {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                      H = ∀ (x : G), x H
                                                      theorem Subgroup.eq_top_iff' {G : Type u_1} [Group G] (H : Subgroup G) :
                                                      H = ∀ (x : G), x H
                                                      def AddSubgroup.closure {G : Type u_1} [AddGroup G] (k : Set G) :

                                                      The AddSubgroup generated by a set

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

                                                        The Subgroup generated by a set.

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

                                                          The AddSubgroup generated by a set includes the set.

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

                                                          The subgroup generated by a set includes the set.

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

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

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

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

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

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

                                                          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 : GProp} {x : G} (h : x Subgroup.closure k) (mem : xk, p x) (one : p 1) (mul : ∀ (x y : G), p xp yp (x * y)) (inv : ∀ (x : G), p xp x⁻¹) :
                                                          p x

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

                                                          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 : (x : G) → x AddSubgroup.closure kProp} (mem : ∀ (x : G) (h : x k), p x ) (one : p 0 ) (mul : ∀ (x : G) (hx : x AddSubgroup.closure k) (y : G) (hy : y AddSubgroup.closure k), p x hxp y hyp (x + y) ) (inv : ∀ (x : G) (hx : x AddSubgroup.closure k), p x hxp (-x) ) {x : G} (hx : x AddSubgroup.closure k) :
                                                          p x hx

                                                          A dependent version of AddSubgroup.closure_induction.

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

                                                          A dependent version of Subgroup.closure_induction.

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

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

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

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

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

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

                                                          Equations
                                                          Instances For
                                                            theorem AddSubgroup.closureAddCommGroupOfComm.proof_1 {G : Type u_1} [AddGroup G] {k : Set G} (hcomm : xk, yk, x + y = y + x) (x : { x : G // x AddSubgroup.closure k }) (y : { x : G // x AddSubgroup.closure k }) :
                                                            x + y = y + x
                                                            def Subgroup.closureCommGroupOfComm {G : Type u_1} [Group G] {k : Set G} (hcomm : xk, yk, x * y = y * x) :
                                                            CommGroup { x : G // x Subgroup.closure k }

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

                                                            Equations
                                                            Instances For
                                                              theorem AddSubgroup.gi.proof_1 (G : Type u_1) [AddGroup G] (_s : AddSubgroup G) :
                                                              _s (AddSubgroup.closure _s)
                                                              theorem AddSubgroup.gi.proof_2 (G : Type u_1) [AddGroup G] (_s : Set G) (_h : (AddSubgroup.closure _s) _s) :
                                                              (fun (s : Set G) (x : (AddSubgroup.closure s) s) => AddSubgroup.closure s) _s _h = (fun (s : Set G) (x : (AddSubgroup.closure s) s) => AddSubgroup.closure s) _s _h
                                                              def AddSubgroup.gi (G : Type u_1) [AddGroup G] :
                                                              GaloisInsertion AddSubgroup.closure SetLike.coe

                                                              closure forms a Galois insertion with the coercion to set.

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

                                                                closure forms a Galois insertion with the coercion to set.

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

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

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

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

                                                                  @[simp]

                                                                  Additive closure of an additive subgroup K equals K

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

                                                                  Closure of a subgroup K equals K.

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

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

                                                                  theorem Subgroup.mem_closure_singleton {G : Type u_1} [Group G] {x : G} {y : G} :
                                                                  y Subgroup.closure {x} ∃ (n : ), x ^ n = y

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

                                                                  @[simp]
                                                                  theorem AddSubgroup.mem_iSup_of_directed {G : Type u_1} [AddGroup G] {ι : Sort u_5} [hι : 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.mem_iSup_of_directed {G : Type u_1} [Group G] {ι : Sort u_5} [hι : 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.coe_iSup_of_directed {G : Type u_1} [AddGroup G] {ι : Sort u_5} [Nonempty ι] {S : ιAddSubgroup G} (hS : Directed (fun (x1 x2 : AddSubgroup G) => x1 x2) S) :
                                                                  (⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
                                                                  theorem Subgroup.coe_iSup_of_directed {G : Type u_1} [Group G] {ι : Sort u_5} [Nonempty ι] {S : ιSubgroup G} (hS : Directed (fun (x1 x2 : Subgroup G) => x1 x2) S) :
                                                                  (⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
                                                                  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_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.comap.proof_1 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] :
                                                                  theorem AddSubgroup.comap.proof_3 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) :
                                                                  0 (AddSubmonoid.comap f H.toAddSubmonoid).carrier
                                                                  def AddSubgroup.comap {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) :

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

                                                                  Equations
                                                                  Instances For
                                                                    theorem AddSubgroup.comap.proof_4 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) {a : G} (ha : a { carrier := f ⁻¹' H, add_mem' := , zero_mem' := }.carrier) :
                                                                    f (-a) H
                                                                    theorem AddSubgroup.comap.proof_2 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) :
                                                                    ∀ {a b : G}, a (AddSubmonoid.comap f H.toAddSubmonoid).carrierb (AddSubmonoid.comap f H.toAddSubmonoid).carriera + b (AddSubmonoid.comap f H.toAddSubmonoid).carrier
                                                                    def Subgroup.comap {G : Type u_1} [Group G] {N : Type u_7} [Group N] (f : G →* N) (H : Subgroup N) :

                                                                    The preimage of a subgroup along a monoid homomorphism is a subgroup.

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem AddSubgroup.coe_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup N) (f : G →+ N) :
                                                                      (AddSubgroup.comap f K) = f ⁻¹' K
                                                                      @[simp]
                                                                      theorem Subgroup.coe_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup N) (f : G →* N) :
                                                                      (Subgroup.comap f K) = f ⁻¹' K
                                                                      @[simp]
                                                                      theorem Subgroup.toAddSubgroup_comap {G : Type u_1} [Group G] {G₂ : Type u_7} [Group G₂] (f : G →* G₂) (s : Subgroup G₂) :
                                                                      AddSubgroup.comap (MonoidHom.toAdditive f) (Subgroup.toAddSubgroup s) = Subgroup.toAddSubgroup (Subgroup.comap f s)
                                                                      @[simp]
                                                                      theorem AddSubgroup.toSubgroup_comap {A : Type u_7} {A₂ : Type u_8} [AddGroup A] [AddGroup A₂] (f : A →+ A₂) (s : AddSubgroup A₂) :
                                                                      Subgroup.comap (AddMonoidHom.toMultiplicative f) (AddSubgroup.toSubgroup s) = AddSubgroup.toSubgroup (AddSubgroup.comap f s)
                                                                      @[simp]
                                                                      theorem AddSubgroup.mem_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {K : AddSubgroup N} {f : G →+ N} {x : G} :
                                                                      @[simp]
                                                                      theorem Subgroup.mem_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {K : Subgroup N} {f : G →* N} {x : G} :
                                                                      theorem AddSubgroup.comap_mono {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup N} {K' : AddSubgroup N} :
                                                                      theorem Subgroup.comap_mono {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup N} {K' : Subgroup N} :
                                                                      theorem AddSubgroup.comap_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {P : Type u_6} [AddGroup P] (K : AddSubgroup P) (g : N →+ P) (f : G →+ N) :
                                                                      theorem Subgroup.comap_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {P : Type u_6} [Group P] (K : Subgroup P) (g : N →* P) (f : G →* N) :
                                                                      @[simp]
                                                                      theorem Subgroup.comap_id {N : Type u_5} [Group N] (K : Subgroup N) :
                                                                      theorem AddSubgroup.map.proof_2 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) :
                                                                      ∀ {a b : N}, a (AddSubmonoid.map f H.toAddSubmonoid).carrierb (AddSubmonoid.map f H.toAddSubmonoid).carriera + b (AddSubmonoid.map f H.toAddSubmonoid).carrier
                                                                      theorem AddSubgroup.map.proof_4 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) :
                                                                      ∀ {x : N}, x { carrier := f '' H, add_mem' := , zero_mem' := }.carrier-x { carrier := f '' H, add_mem' := , zero_mem' := }.carrier
                                                                      def AddSubgroup.map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) :

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

                                                                      Equations
                                                                      • AddSubgroup.map f H = { carrier := f '' H, add_mem' := , zero_mem' := , neg_mem' := }
                                                                      Instances For
                                                                        theorem AddSubgroup.map.proof_3 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) :
                                                                        0 (AddSubmonoid.map f H.toAddSubmonoid).carrier
                                                                        theorem AddSubgroup.map.proof_1 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] :
                                                                        def Subgroup.map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) :

                                                                        The image of a subgroup along a monoid homomorphism is a subgroup.

                                                                        Equations
                                                                        • Subgroup.map f H = { carrier := f '' H, mul_mem' := , one_mem' := , inv_mem' := }
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem AddSubgroup.coe_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (K : AddSubgroup G) :
                                                                          (AddSubgroup.map f K) = f '' K
                                                                          @[simp]
                                                                          theorem Subgroup.coe_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (K : Subgroup G) :
                                                                          (Subgroup.map f K) = f '' K
                                                                          @[simp]
                                                                          theorem AddSubgroup.mem_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup G} {y : N} :
                                                                          y AddSubgroup.map f K xK, f x = y
                                                                          @[simp]
                                                                          theorem Subgroup.mem_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup G} {y : N} :
                                                                          y Subgroup.map f K xK, f x = y
                                                                          theorem AddSubgroup.mem_map_of_mem {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {K : AddSubgroup G} {x : G} (hx : x K) :
                                                                          theorem Subgroup.mem_map_of_mem {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {K : Subgroup G} {x : G} (hx : x K) :
                                                                          theorem AddSubgroup.apply_coe_mem_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (K : AddSubgroup G) (x : { x : G // x K }) :
                                                                          f x AddSubgroup.map f K
                                                                          theorem Subgroup.apply_coe_mem_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (K : Subgroup G) (x : { x : G // x K }) :
                                                                          f x Subgroup.map f K
                                                                          theorem AddSubgroup.map_mono {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup G} {K' : AddSubgroup G} :
                                                                          theorem Subgroup.map_mono {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup G} {K' : Subgroup G} :
                                                                          K K'Subgroup.map f K Subgroup.map f K'
                                                                          @[simp]
                                                                          @[simp]
                                                                          theorem Subgroup.map_id {G : Type u_1} [Group G] (K : Subgroup G) :
                                                                          theorem AddSubgroup.map_map {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] {P : Type u_6} [AddGroup P] (g : N →+ P) (f : G →+ N) :
                                                                          theorem Subgroup.map_map {G : Type u_1} [Group G] (K : Subgroup G) {N : Type u_5} [Group N] {P : Type u_6} [Group P] (g : N →* P) (f : G →* N) :
                                                                          @[simp]
                                                                          theorem AddSubgroup.map_zero_eq_bot {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] :
                                                                          @[simp]
                                                                          theorem Subgroup.map_one_eq_bot {G : Type u_1} [Group G] (K : Subgroup G) {N : Type u_5} [Group N] :
                                                                          theorem AddSubgroup.mem_map_equiv {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G ≃+ N} {K : AddSubgroup G} {x : N} :
                                                                          x AddSubgroup.map f.toAddMonoidHom K f.symm x K
                                                                          theorem Subgroup.mem_map_equiv {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G ≃* N} {K : Subgroup G} {x : N} :
                                                                          x Subgroup.map f.toMonoidHom K f.symm x K
                                                                          @[simp]
                                                                          theorem AddSubgroup.mem_map_iff_mem {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective f) {K : AddSubgroup G} {x : G} :
                                                                          @[simp]
                                                                          theorem Subgroup.mem_map_iff_mem {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective f) {K : Subgroup G} {x : G} :
                                                                          f x Subgroup.map f K x K
                                                                          theorem AddSubgroup.map_equiv_eq_comap_symm' {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G ≃+ N) (K : AddSubgroup G) :
                                                                          AddSubgroup.map f.toAddMonoidHom K = AddSubgroup.comap f.symm.toAddMonoidHom K
                                                                          theorem Subgroup.map_equiv_eq_comap_symm' {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G ≃* N) (K : Subgroup G) :
                                                                          Subgroup.map f.toMonoidHom K = Subgroup.comap f.symm.toMonoidHom K
                                                                          theorem AddSubgroup.map_equiv_eq_comap_symm {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G ≃+ N) (K : AddSubgroup G) :
                                                                          AddSubgroup.map (↑f) K = AddSubgroup.comap (↑f.symm) K
                                                                          theorem Subgroup.map_equiv_eq_comap_symm {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G ≃* N) (K : Subgroup G) :
                                                                          Subgroup.map (↑f) K = Subgroup.comap (↑f.symm) K
                                                                          theorem AddSubgroup.comap_equiv_eq_map_symm {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : N ≃+ G) (K : AddSubgroup G) :
                                                                          AddSubgroup.comap (↑f) K = AddSubgroup.map (↑f.symm) K
                                                                          theorem Subgroup.comap_equiv_eq_map_symm {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : N ≃* G) (K : Subgroup G) :
                                                                          Subgroup.comap (↑f) K = Subgroup.map (↑f.symm) K
                                                                          theorem AddSubgroup.comap_equiv_eq_map_symm' {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : N ≃+ G) (K : AddSubgroup G) :
                                                                          AddSubgroup.comap f.toAddMonoidHom K = AddSubgroup.map f.symm.toAddMonoidHom K
                                                                          theorem Subgroup.comap_equiv_eq_map_symm' {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : N ≃* G) (K : Subgroup G) :
                                                                          Subgroup.comap f.toMonoidHom K = Subgroup.map f.symm.toMonoidHom K
                                                                          theorem AddSubgroup.map_symm_eq_iff_map_eq {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] {H : AddSubgroup N} {e : G ≃+ N} :
                                                                          AddSubgroup.map (↑e.symm) H = K AddSubgroup.map (↑e) K = H
                                                                          theorem Subgroup.map_symm_eq_iff_map_eq {G : Type u_1} [Group G] (K : Subgroup G) {N : Type u_5} [Group N] {H : Subgroup N} {e : G ≃* N} :
                                                                          Subgroup.map (↑e.symm) H = K Subgroup.map (↑e) K = H
                                                                          theorem AddSubgroup.map_le_iff_le_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup G} {H : AddSubgroup N} :
                                                                          theorem Subgroup.map_le_iff_le_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup G} {H : Subgroup N} :
                                                                          theorem Subgroup.gc_map_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                                                                          theorem AddSubgroup.map_sup {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup G) (f : G →+ N) :
                                                                          theorem Subgroup.map_sup {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup G) (f : G →* N) :
                                                                          theorem AddSubgroup.map_iSup {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ιAddSubgroup G) :
                                                                          AddSubgroup.map f (iSup s) = ⨆ (i : ι), AddSubgroup.map f (s i)
                                                                          theorem Subgroup.map_iSup {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} (f : G →* N) (s : ιSubgroup G) :
                                                                          Subgroup.map f (iSup s) = ⨆ (i : ι), Subgroup.map f (s i)
                                                                          theorem Subgroup.comap_sup_comap_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup N) (K : Subgroup N) (f : G →* N) :
                                                                          theorem AddSubgroup.iSup_comap_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ιAddSubgroup N) :
                                                                          ⨆ (i : ι), AddSubgroup.comap f (s i) AddSubgroup.comap f (iSup s)
                                                                          theorem Subgroup.iSup_comap_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} (f : G →* N) (s : ιSubgroup N) :
                                                                          ⨆ (i : ι), Subgroup.comap f (s i) Subgroup.comap f (iSup s)
                                                                          theorem AddSubgroup.comap_inf {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup N) (K : AddSubgroup N) (f : G →+ N) :
                                                                          theorem Subgroup.comap_inf {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup N) (K : Subgroup N) (f : G →* N) :
                                                                          theorem AddSubgroup.comap_iInf {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ιAddSubgroup N) :
                                                                          AddSubgroup.comap f (iInf s) = ⨅ (i : ι), AddSubgroup.comap f (s i)
                                                                          theorem Subgroup.comap_iInf {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} (f : G →* N) (s : ιSubgroup N) :
                                                                          Subgroup.comap f (iInf s) = ⨅ (i : ι), Subgroup.comap f (s i)
                                                                          theorem AddSubgroup.map_inf_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup G) (f : G →+ N) :
                                                                          theorem Subgroup.map_inf_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup G) (f : G →* N) :
                                                                          theorem AddSubgroup.map_inf_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup G) (f : G →+ N) (hf : Function.Injective f) :
                                                                          theorem Subgroup.map_inf_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
                                                                          @[simp]
                                                                          theorem AddSubgroup.map_bot {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                                                                          @[simp]
                                                                          theorem Subgroup.map_bot {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                                                                          @[simp]
                                                                          theorem AddSubgroup.map_top_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (h : Function.Surjective f) :
                                                                          @[simp]
                                                                          theorem Subgroup.map_top_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (h : Function.Surjective f) :
                                                                          @[simp]
                                                                          theorem AddSubgroup.comap_top {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                                                                          @[simp]
                                                                          theorem Subgroup.comap_top {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                                                                          def AddSubgroup.addSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) :
                                                                          AddSubgroup { x : G // x K }

                                                                          For any subgroups H and K, view H ⊓ K as a subgroup of K.

                                                                          Equations
                                                                          Instances For
                                                                            def Subgroup.subgroupOf {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) :
                                                                            Subgroup { x : G // x K }

                                                                            For any subgroups H and K, view H ⊓ K as a subgroup of K.

                                                                            Equations
                                                                            Instances For
                                                                              theorem AddSubgroup.addSubgroupOfEquivOfLe.proof_2 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) (g : { x : G // x H }) :
                                                                              g K
                                                                              def AddSubgroup.addSubgroupOfEquivOfLe {G : Type u_7} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) :
                                                                              { x : { x : G // x K } // x H.addSubgroupOf K } ≃+ { x : G // x H }

                                                                              If H ≤ K, then H as a subgroup of K is isomorphic to H.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                theorem AddSubgroup.addSubgroupOfEquivOfLe.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (g : { x : { x : G // x K } // x H.addSubgroupOf K }) :
                                                                                g H.addSubgroupOf K
                                                                                theorem AddSubgroup.addSubgroupOfEquivOfLe.proof_4 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) (_g : { x : { x : G // x K } // x H.addSubgroupOf K }) :
                                                                                (fun (g : { x : G // x H }) => g, , ) ((fun (g : { x : { x : G // x K } // x H.addSubgroupOf K }) => g, ) _g) = _g
                                                                                theorem AddSubgroup.addSubgroupOfEquivOfLe.proof_6 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) (_g : { x : { x : G // x K } // x H.addSubgroupOf K }) (_h : { x : { x : G // x K } // x H.addSubgroupOf K }) :
                                                                                { toFun := fun (g : { x : { x : G // x K } // x H.addSubgroupOf K }) => g, , invFun := fun (g : { x : G // x H }) => g, , , left_inv := , right_inv := }.toFun (_g + _h) = { toFun := fun (g : { x : { x : G // x K } // x H.addSubgroupOf K }) => g, , invFun := fun (g : { x : G // x H }) => g, , , left_inv := , right_inv := }.toFun (_g + _h)
                                                                                theorem AddSubgroup.addSubgroupOfEquivOfLe.proof_3 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (g : { x : G // x H }) :
                                                                                g H
                                                                                theorem AddSubgroup.addSubgroupOfEquivOfLe.proof_5 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) (_g : { x : G // x H }) :
                                                                                (fun (g : { x : { x : G // x K } // x H.addSubgroupOf K }) => g, ) ((fun (g : { x : G // x H }) => g, , ) _g) = _g
                                                                                @[simp]
                                                                                theorem Subgroup.subgroupOfEquivOfLe_symm_apply_coe_coe {G : Type u_7} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H K) (g : { x : G // x H }) :
                                                                                ((Subgroup.subgroupOfEquivOfLe h).symm g) = g
                                                                                @[simp]
                                                                                theorem AddSubgroup.addSubgroupOfEquivOfLe_symm_apply_coe_coe {G : Type u_7} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) (g : { x : G // x H }) :
                                                                                ((AddSubgroup.addSubgroupOfEquivOfLe h).symm g) = g
                                                                                @[simp]
                                                                                theorem AddSubgroup.addSubgroupOfEquivOfLe_apply_coe {G : Type u_7} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) (g : { x : { x : G // x K } // x H.addSubgroupOf K }) :
                                                                                @[simp]
                                                                                theorem Subgroup.subgroupOfEquivOfLe_apply_coe {G : Type u_7} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H K) (g : { x : { x : G // x K } // x H.subgroupOf K }) :
                                                                                ((Subgroup.subgroupOfEquivOfLe h) g) = g
                                                                                def Subgroup.subgroupOfEquivOfLe {G : Type u_7} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H K) :
                                                                                { x : { x : G // x K } // x H.subgroupOf K } ≃* { x : G // x H }

                                                                                If H ≤ K, then H as a subgroup of K is isomorphic to H.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem AddSubgroup.comap_subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) :
                                                                                  AddSubgroup.comap K.subtype H = H.addSubgroupOf K
                                                                                  @[simp]
                                                                                  theorem Subgroup.comap_subtype {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) :
                                                                                  Subgroup.comap K.subtype H = H.subgroupOf K
                                                                                  @[simp]
                                                                                  theorem AddSubgroup.comap_inclusion_addSubgroupOf {G : Type u_1} [AddGroup G] {K₁ : AddSubgroup G} {K₂ : AddSubgroup G} (h : K₁ K₂) (H : AddSubgroup G) :
                                                                                  AddSubgroup.comap (AddSubgroup.inclusion h) (H.addSubgroupOf K₂) = H.addSubgroupOf K₁
                                                                                  @[simp]
                                                                                  theorem Subgroup.comap_inclusion_subgroupOf {G : Type u_1} [Group G] {K₁ : Subgroup G} {K₂ : Subgroup G} (h : K₁ K₂) (H : Subgroup G) :
                                                                                  Subgroup.comap (Subgroup.inclusion h) (H.subgroupOf K₂) = H.subgroupOf K₁
                                                                                  theorem AddSubgroup.coe_addSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) :
                                                                                  (H.addSubgroupOf K) = K.subtype ⁻¹' H
                                                                                  theorem Subgroup.coe_subgroupOf {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) :
                                                                                  (H.subgroupOf K) = K.subtype ⁻¹' H
                                                                                  theorem AddSubgroup.mem_addSubgroupOf {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {h : { x : G // x K }} :
                                                                                  h H.addSubgroupOf K h H
                                                                                  theorem Subgroup.mem_subgroupOf {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {h : { x : G // x K }} :
                                                                                  h H.subgroupOf K h H
                                                                                  @[simp]
                                                                                  theorem AddSubgroup.addSubgroupOf_map_subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) :
                                                                                  AddSubgroup.map K.subtype (H.addSubgroupOf K) = H K
                                                                                  @[simp]
                                                                                  theorem Subgroup.subgroupOf_map_subtype {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) :
                                                                                  Subgroup.map K.subtype (H.subgroupOf K) = H K
                                                                                  @[simp]
                                                                                  theorem AddSubgroup.bot_addSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                                                  .addSubgroupOf H =
                                                                                  @[simp]
                                                                                  theorem Subgroup.bot_subgroupOf {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                  .subgroupOf H =
                                                                                  @[simp]
                                                                                  theorem AddSubgroup.top_addSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                                                  .addSubgroupOf H =
                                                                                  @[simp]
                                                                                  theorem Subgroup.top_subgroupOf {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                  .subgroupOf H =
                                                                                  theorem AddSubgroup.addSubgroupOf_bot_eq_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                                                  H.addSubgroupOf =
                                                                                  theorem Subgroup.subgroupOf_bot_eq_bot {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                  H.subgroupOf =
                                                                                  theorem AddSubgroup.addSubgroupOf_bot_eq_top {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                                                  H.addSubgroupOf =
                                                                                  theorem Subgroup.subgroupOf_bot_eq_top {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                  H.subgroupOf =
                                                                                  @[simp]
                                                                                  theorem AddSubgroup.addSubgroupOf_self {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                                                  H.addSubgroupOf H =
                                                                                  @[simp]
                                                                                  theorem Subgroup.subgroupOf_self {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                  H.subgroupOf H =
                                                                                  @[simp]
                                                                                  theorem AddSubgroup.addSubgroupOf_inj {G : Type u_1} [AddGroup G] {H₁ : AddSubgroup G} {H₂ : AddSubgroup G} {K : AddSubgroup G} :
                                                                                  H₁.addSubgroupOf K = H₂.addSubgroupOf K H₁ K = H₂ K
                                                                                  @[simp]
                                                                                  theorem Subgroup.subgroupOf_inj {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} {K : Subgroup G} :
                                                                                  H₁.subgroupOf K = H₂.subgroupOf K H₁ K = H₂ K
                                                                                  @[simp]
                                                                                  theorem AddSubgroup.inf_addSubgroupOf_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) :
                                                                                  (H K).addSubgroupOf K = H.addSubgroupOf K
                                                                                  @[simp]
                                                                                  theorem Subgroup.inf_subgroupOf_right {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) :
                                                                                  (H K).subgroupOf K = H.subgroupOf K
                                                                                  @[simp]
                                                                                  theorem AddSubgroup.inf_addSubgroupOf_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) :
                                                                                  (K H).addSubgroupOf K = H.addSubgroupOf K
                                                                                  @[simp]
                                                                                  theorem Subgroup.inf_subgroupOf_left {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) :
                                                                                  (K H).subgroupOf K = H.subgroupOf K
                                                                                  @[simp]
                                                                                  theorem AddSubgroup.addSubgroupOf_eq_bot {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} :
                                                                                  H.addSubgroupOf K = Disjoint H K
                                                                                  @[simp]
                                                                                  theorem Subgroup.subgroupOf_eq_bot {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} :
                                                                                  H.subgroupOf K = Disjoint H K
                                                                                  @[simp]
                                                                                  theorem AddSubgroup.addSubgroupOf_eq_top {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} :
                                                                                  H.addSubgroupOf K = K H
                                                                                  @[simp]
                                                                                  theorem Subgroup.subgroupOf_eq_top {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} :
                                                                                  H.subgroupOf K = K H
                                                                                  theorem AddSubgroup.prod.proof_1 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) :
                                                                                  ∀ {x : G × N}, x (H.prod K.toAddSubmonoid).carrier(-x).1 H.toAddSubmonoid (-x).2 K.toAddSubmonoid
                                                                                  def AddSubgroup.prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) :

                                                                                  Given AddSubgroups H, K of AddGroups A, B respectively, H × K as an AddSubgroup of A × B.

                                                                                  Equations
                                                                                  • H.prod K = { toAddSubmonoid := H.prod K.toAddSubmonoid, neg_mem' := }
                                                                                  Instances For
                                                                                    def Subgroup.prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup N) :
                                                                                    Subgroup (G × N)

                                                                                    Given Subgroups H, K of groups G, N respectively, H × K as a subgroup of G × N.

                                                                                    Equations
                                                                                    • H.prod K = { toSubmonoid := H.prod K.toSubmonoid, inv_mem' := }
                                                                                    Instances For
                                                                                      theorem AddSubgroup.coe_prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) :
                                                                                      (H.prod K) = H ×ˢ K
                                                                                      theorem Subgroup.coe_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup N) :
                                                                                      (H.prod K) = H ×ˢ K
                                                                                      theorem AddSubgroup.mem_prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} {p : G × N} :
                                                                                      p H.prod K p.1 H p.2 K
                                                                                      theorem Subgroup.mem_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} {p : G × N} :
                                                                                      p H.prod K p.1 H p.2 K
                                                                                      theorem AddSubgroup.prod_mono {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] :
                                                                                      ((fun (x1 x2 : AddSubgroup G) => x1 x2) (fun (x1 x2 : AddSubgroup N) => x1 x2) fun (x1 x2 : AddSubgroup (G × N)) => x1 x2) AddSubgroup.prod AddSubgroup.prod
                                                                                      theorem Subgroup.prod_mono {G : Type u_1} [Group G] {N : Type u_5} [Group N] :
                                                                                      ((fun (x1 x2 : Subgroup G) => x1 x2) (fun (x1 x2 : Subgroup N) => x1 x2) fun (x1 x2 : Subgroup (G × N)) => x1 x2) Subgroup.prod Subgroup.prod
                                                                                      theorem AddSubgroup.prod_mono_right {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) :
                                                                                      Monotone fun (t : AddSubgroup N) => K.prod t
                                                                                      theorem Subgroup.prod_mono_right {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) :
                                                                                      Monotone fun (t : Subgroup N) => K.prod t
                                                                                      theorem AddSubgroup.prod_mono_left {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup N) :
                                                                                      Monotone fun (K : AddSubgroup G) => K.prod H
                                                                                      theorem Subgroup.prod_mono_left {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup N) :
                                                                                      Monotone fun (K : Subgroup G) => K.prod H
                                                                                      theorem AddSubgroup.prod_top {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) :
                                                                                      theorem Subgroup.prod_top {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) :
                                                                                      theorem AddSubgroup.top_prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup N) :
                                                                                      theorem Subgroup.top_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup N) :
                                                                                      @[simp]
                                                                                      theorem AddSubgroup.top_prod_top {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] :
                                                                                      .prod =
                                                                                      @[simp]
                                                                                      theorem Subgroup.top_prod_top {G : Type u_1} [Group G] {N : Type u_5} [Group N] :
                                                                                      .prod =
                                                                                      theorem AddSubgroup.bot_sum_bot {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] :
                                                                                      .prod =
                                                                                      theorem Subgroup.bot_prod_bot {G : Type u_1} [Group G] {N : Type u_5} [Group N] :
                                                                                      .prod =
                                                                                      theorem AddSubgroup.le_prod_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} {J : AddSubgroup (G × N)} :
                                                                                      theorem Subgroup.le_prod_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
                                                                                      theorem AddSubgroup.prod_le_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} {J : AddSubgroup (G × N)} :
                                                                                      theorem Subgroup.prod_le_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} :
                                                                                      @[simp]
                                                                                      theorem AddSubgroup.prod_eq_bot_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} :
                                                                                      H.prod K = H = K =
                                                                                      @[simp]
                                                                                      theorem Subgroup.prod_eq_bot_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} :
                                                                                      H.prod K = H = K =
                                                                                      theorem AddSubgroup.prodEquiv.proof_1 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) :
                                                                                      ∀ (x x_1 : { x : G × N // x H.prod K }), (Equiv.Set.prod H K).toFun (x + x_1) = (Equiv.Set.prod H K).toFun (x + x_1)
                                                                                      def AddSubgroup.prodEquiv {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) :
                                                                                      { x : G × N // x H.prod K } ≃+ { x : G // x H } × { x : N // x K }

                                                                                      Product of additive subgroups is isomorphic to their product as additive groups

                                                                                      Equations
                                                                                      Instances For
                                                                                        def Subgroup.prodEquiv {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup N) :
                                                                                        { x : G × N // x H.prod K } ≃* { x : G // x H } × { x : N // x K }

                                                                                        Product of subgroups is isomorphic to their product as groups.

                                                                                        Equations
                                                                                        Instances For
                                                                                          theorem AddSubmonoid.pi.proof_1 {η : Type u_1} {f : ηType u_2} [(i : η) → AddZeroClass (f i)] (I : Set η) (s : (i : η) → AddSubmonoid (f i)) :
                                                                                          ∀ {a b : (i : η) → f i}, (a I.pi fun (i : η) => (s i).carrier)(b I.pi fun (i : η) => (s i).carrier)iI, a i + b i s i
                                                                                          def AddSubmonoid.pi {η : Type u_7} {f : ηType u_8} [(i : η) → AddZeroClass (f i)] (I : Set η) (s : (i : η) → AddSubmonoid (f i)) :
                                                                                          AddSubmonoid ((i : η) → f i)

                                                                                          A version of Set.pi for AddSubmonoids. Given an index set I and a family of submodules s : Π i, AddSubmonoid f i, pi I s is the AddSubmonoid of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I.

                                                                                          Equations
                                                                                          • AddSubmonoid.pi I s = { carrier := I.pi fun (i : η) => (s i).carrier, add_mem' := , zero_mem' := }
                                                                                          Instances For
                                                                                            theorem AddSubmonoid.pi.proof_2 {η : Type u_1} {f : ηType u_2} [(i : η) → AddZeroClass (f i)] (I : Set η) (s : (i : η) → AddSubmonoid (f i)) (i : η) :
                                                                                            i I0 s i
                                                                                            def Submonoid.pi {η : Type u_7} {f : ηType u_8} [(i : η) → MulOneClass (f i)] (I : Set η) (s : (i : η) → Submonoid (f i)) :
                                                                                            Submonoid ((i : η) → f i)

                                                                                            A version of Set.pi for submonoids. Given an index set I and a family of submodules s : Π i, Submonoid f i, pi I s is the submonoid of dependent functions f : Π i, f i such that f i belongs to Pi I s whenever i ∈ I.

                                                                                            Equations
                                                                                            • Submonoid.pi I s = { carrier := I.pi fun (i : η) => (s i).carrier, mul_mem' := , one_mem' := }
                                                                                            Instances For
                                                                                              theorem AddSubgroup.pi.proof_1 {η : Type u_1} {f : ηType u_2} [(i : η) → AddGroup (f i)] (I : Set η) (H : (i : η) → AddSubgroup (f i)) :
                                                                                              ∀ {x : (i : η) → f i}, x (AddSubmonoid.pi I fun (i : η) => (H i).toAddSubmonoid).carrieriI, -x i H i
                                                                                              def AddSubgroup.pi {η : Type u_7} {f : ηType u_8} [(i : η) → AddGroup (f i)] (I : Set η) (H : (i : η) → AddSubgroup (f i)) :
                                                                                              AddSubgroup ((i : η) → f i)

                                                                                              A version of Set.pi for AddSubgroups. Given an index set I and a family of submodules s : Π i, AddSubgroup f i, pi I s is the AddSubgroup of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I.

                                                                                              Equations
                                                                                              Instances For
                                                                                                def Subgroup.pi {η : Type u_7} {f : ηType u_8} [(i : η) → Group (f i)] (I : Set η) (H : (i : η) → Subgroup (f i)) :
                                                                                                Subgroup ((i : η) → f i)

                                                                                                A version of Set.pi for subgroups. Given an index set I and a family of submodules s : Π i, Subgroup f i, pi I s is the subgroup of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  theorem AddSubgroup.coe_pi {η : Type u_7} {f : ηType u_8} [(i : η) → AddGroup (f i)] (I : Set η) (H : (i : η) → AddSubgroup (f i)) :
                                                                                                  (AddSubgroup.pi I H) = I.pi fun (i : η) => (H i)
                                                                                                  theorem Subgroup.coe_pi {η : Type u_7} {f : ηType u_8} [(i : η) → Group (f i)] (I : Set η) (H : (i : η) → Subgroup (f i)) :
                                                                                                  (Subgroup.pi I H) = I.pi fun (i : η) => (H i)
                                                                                                  theorem AddSubgroup.mem_pi {η : Type u_7} {f : ηType u_8} [(i : η) → AddGroup (f i)] (I : Set η) {H : (i : η) → AddSubgroup (f i)} {p : (i : η) → f i} :
                                                                                                  p AddSubgroup.pi I H iI, p i H i
                                                                                                  theorem Subgroup.mem_pi {η : Type u_7} {f : ηType u_8} [(i : η) → Group (f i)] (I : Set η) {H : (i : η) → Subgroup (f i)} {p : (i : η) → f i} :
                                                                                                  p Subgroup.pi I H iI, p i H i
                                                                                                  theorem AddSubgroup.pi_top {η : Type u_7} {f : ηType u_8} [(i : η) → AddGroup (f i)] (I : Set η) :
                                                                                                  (AddSubgroup.pi I fun (i : η) => ) =
                                                                                                  theorem Subgroup.pi_top {η : Type u_7} {f : ηType u_8} [(i : η) → Group (f i)] (I : Set η) :
                                                                                                  (Subgroup.pi I fun (i : η) => ) =
                                                                                                  theorem AddSubgroup.pi_empty {η : Type u_7} {f : ηType u_8} [(i : η) → AddGroup (f i)] (H : (i : η) → AddSubgroup (f i)) :
                                                                                                  theorem Subgroup.pi_empty {η : Type u_7} {f : ηType u_8} [(i : η) → Group (f i)] (H : (i : η) → Subgroup (f i)) :
                                                                                                  theorem AddSubgroup.pi_bot {η : Type u_7} {f : ηType u_8} [(i : η) → AddGroup (f i)] :
                                                                                                  (AddSubgroup.pi Set.univ fun (i : η) => ) =
                                                                                                  theorem Subgroup.pi_bot {η : Type u_7} {f : ηType u_8} [(i : η) → Group (f i)] :
                                                                                                  (Subgroup.pi Set.univ fun (i : η) => ) =
                                                                                                  theorem AddSubgroup.le_pi_iff {η : Type u_7} {f : ηType u_8} [(i : η) → AddGroup (f i)] {I : Set η} {H : (i : η) → AddSubgroup (f i)} {J : AddSubgroup ((i : η) → f i)} :
                                                                                                  theorem Subgroup.le_pi_iff {η : Type u_7} {f : ηType u_8} [(i : η) → Group (f i)] {I : Set η} {H : (i : η) → Subgroup (f i)} {J : Subgroup ((i : η) → f i)} :
                                                                                                  J Subgroup.pi I H iI, Subgroup.map (Pi.evalMonoidHom f i) J H i
                                                                                                  @[simp]
                                                                                                  theorem AddSubgroup.single_mem_pi {η : Type u_7} {f : ηType u_8} [(i : η) → AddGroup (f i)] [DecidableEq η] {I : Set η} {H : (i : η) → AddSubgroup (f i)} (i : η) (x : f i) :
                                                                                                  Pi.single i x AddSubgroup.pi I H i Ix H i
                                                                                                  @[simp]
                                                                                                  theorem Subgroup.mulSingle_mem_pi {η : Type u_7} {f : ηType u_8} [(i : η) → Group (f i)] [DecidableEq η] {I : Set η} {H : (i : η) → Subgroup (f i)} (i : η) (x : f i) :
                                                                                                  Pi.mulSingle i x Subgroup.pi I H i Ix H i
                                                                                                  theorem AddSubgroup.pi_eq_bot_iff {η : Type u_7} {f : ηType u_8} [(i : η) → AddGroup (f i)] (H : (i : η) → AddSubgroup (f i)) :
                                                                                                  AddSubgroup.pi Set.univ H = ∀ (i : η), H i =
                                                                                                  theorem Subgroup.pi_eq_bot_iff {η : Type u_7} {f : ηType u_8} [(i : η) → Group (f i)] (H : (i : η) → Subgroup (f i)) :
                                                                                                  Subgroup.pi Set.univ H = ∀ (i : η), H i =
                                                                                                  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 : nH, ∀ (g : G), g * n * g⁻¹ H

                                                                                                    N is closed under conjugation

                                                                                                  Instances
                                                                                                    theorem Subgroup.Normal.conj_mem {G : Type u_1} [Group G] {H : Subgroup G} (self : H.Normal) (n : G) :
                                                                                                    n H∀ (g : G), g * n * g⁻¹ H

                                                                                                    N is closed under conjugation

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

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

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

                                                                                                      N is closed under additive conjugation

                                                                                                    Instances
                                                                                                      theorem AddSubgroup.Normal.conj_mem {A : Type u_4} [AddGroup A] {H : AddSubgroup A} (self : H.Normal) (n : A) :
                                                                                                      n H∀ (g : A), g + n + -g H

                                                                                                      N is closed under additive conjugation

                                                                                                      @[instance 100]
                                                                                                      instance AddSubgroup.normal_of_comm {G : Type u_5} [AddCommGroup G] (H : AddSubgroup G) :
                                                                                                      H.Normal
                                                                                                      Equations
                                                                                                      • =
                                                                                                      @[instance 100]
                                                                                                      instance Subgroup.normal_of_comm {G : Type u_5} [CommGroup G] (H : Subgroup G) :
                                                                                                      H.Normal
                                                                                                      Equations
                                                                                                      • =
                                                                                                      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.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.mem_comm {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (nH : H.Normal) {a : G} {b : G} (h : a + b H) :
                                                                                                      b + a H
                                                                                                      theorem Subgroup.Normal.mem_comm {G : Type u_1} [Group G] {H : Subgroup G} (nH : H.Normal) {a : G} {b : G} (h : 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 : G} {b : G} :
                                                                                                      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 : G} {b : G} :
                                                                                                      a * b H b * a H
                                                                                                      class Subgroup.Characteristic {G : Type u_1} [Group G] (H : Subgroup G) :

                                                                                                      A subgroup is characteristic if it is fixed by all automorphisms. Several equivalent conditions are provided by lemmas of the form Characteristic.iff...

                                                                                                      • fixed : ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H = H

                                                                                                        H is fixed by all automorphisms

                                                                                                      Instances
                                                                                                        theorem Subgroup.Characteristic.fixed {G : Type u_1} [Group G] {H : Subgroup G} (self : H.Characteristic) (ϕ : G ≃* G) :
                                                                                                        Subgroup.comap ϕ.toMonoidHom H = H

                                                                                                        H is fixed by all automorphisms

                                                                                                        @[instance 100]
                                                                                                        instance Subgroup.normal_of_characteristic {G : Type u_1} [Group G] (H : Subgroup G) [h : H.Characteristic] :
                                                                                                        H.Normal
                                                                                                        Equations
                                                                                                        • =

                                                                                                        An AddSubgroup is characteristic if it is fixed by all automorphisms. Several equivalent conditions are provided by lemmas of the form Characteristic.iff...

                                                                                                        Instances
                                                                                                          theorem AddSubgroup.Characteristic.fixed {A : Type u_4} [AddGroup A] {H : AddSubgroup A} (self : H.Characteristic) (ϕ : A ≃+ A) :
                                                                                                          AddSubgroup.comap ϕ.toAddMonoidHom H = H

                                                                                                          H is fixed by all automorphisms

                                                                                                          @[instance 100]
                                                                                                          instance AddSubgroup.normal_of_characteristic {A : Type u_4} [AddGroup A] (H : AddSubgroup A) [h : H.Characteristic] :
                                                                                                          H.Normal
                                                                                                          Equations
                                                                                                          • =
                                                                                                          theorem AddSubgroup.characteristic_iff_comap_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                                                                          H.Characteristic ∀ (ϕ : G ≃+ G), AddSubgroup.comap ϕ.toAddMonoidHom H = H
                                                                                                          theorem Subgroup.characteristic_iff_comap_eq {G : Type u_1} [Group G] {H : Subgroup G} :
                                                                                                          H.Characteristic ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H = H
                                                                                                          theorem AddSubgroup.characteristic_iff_comap_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                                                                          H.Characteristic ∀ (ϕ : G ≃+ G), AddSubgroup.comap ϕ.toAddMonoidHom H H
                                                                                                          theorem Subgroup.characteristic_iff_comap_le {G : Type u_1} [Group G] {H : Subgroup G} :
                                                                                                          H.Characteristic ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H H
                                                                                                          theorem AddSubgroup.characteristic_iff_le_comap {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                                                                          H.Characteristic ∀ (ϕ : G ≃+ G), H AddSubgroup.comap ϕ.toAddMonoidHom H
                                                                                                          theorem Subgroup.characteristic_iff_le_comap {G : Type u_1} [Group G] {H : Subgroup G} :
                                                                                                          H.Characteristic ∀ (ϕ : G ≃* G), H Subgroup.comap ϕ.toMonoidHom H
                                                                                                          theorem AddSubgroup.characteristic_iff_map_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                                                                          H.Characteristic ∀ (ϕ : G ≃+ G), AddSubgroup.map ϕ.toAddMonoidHom H = H
                                                                                                          theorem Subgroup.characteristic_iff_map_eq {G : Type u_1} [Group G] {H : Subgroup G} :
                                                                                                          H.Characteristic ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom H = H
                                                                                                          theorem AddSubgroup.characteristic_iff_map_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                                                                          H.Characteristic ∀ (ϕ : G ≃+ G), AddSubgroup.map ϕ.toAddMonoidHom H H
                                                                                                          theorem Subgroup.characteristic_iff_map_le {G : Type u_1} [Group G] {H : Subgroup G} :
                                                                                                          H.Characteristic ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom H H
                                                                                                          theorem AddSubgroup.characteristic_iff_le_map {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                                                                          H.Characteristic ∀ (ϕ : G ≃+ G), H AddSubgroup.map ϕ.toAddMonoidHom H
                                                                                                          theorem Subgroup.characteristic_iff_le_map {G : Type u_1} [Group G] {H : Subgroup G} :
                                                                                                          H.Characteristic ∀ (ϕ : G ≃* G), H Subgroup.map ϕ.toMonoidHom H
                                                                                                          instance AddSubgroup.botCharacteristic {G : Type u_1} [AddGroup G] :
                                                                                                          .Characteristic
                                                                                                          Equations
                                                                                                          • =
                                                                                                          instance Subgroup.botCharacteristic {G : Type u_1} [Group G] :
                                                                                                          .Characteristic
                                                                                                          Equations
                                                                                                          • =
                                                                                                          instance AddSubgroup.topCharacteristic {G : Type u_1} [AddGroup G] :
                                                                                                          .Characteristic
                                                                                                          Equations
                                                                                                          • =
                                                                                                          instance Subgroup.topCharacteristic {G : Type u_1} [Group G] :
                                                                                                          .Characteristic
                                                                                                          Equations
                                                                                                          • =
                                                                                                          theorem AddSubgroup.normalizer.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (a : G) :
                                                                                                          a H 0 + a + -0 H

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

                                                                                                          Equations
                                                                                                          • H.normalizer = { carrier := {g : G | ∀ (n : G), n H g + n + -g H}, add_mem' := , zero_mem' := , neg_mem' := }
                                                                                                          Instances For
                                                                                                            theorem AddSubgroup.normalizer.proof_3 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {a : G} (ha : ∀ (n : G), n H a + n + -a H) (n : G) :
                                                                                                            n H -a + n + - -a H
                                                                                                            theorem AddSubgroup.normalizer.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {a : G} {b : G} (ha : ∀ (n : G), n H a + n + -a H) (hb : ∀ (n : G), n H b + n + -b H) (n : G) :
                                                                                                            n H a + b + n + -(a + b) 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
                                                                                                            • H.normalizer = { carrier := {g : G | ∀ (n : G), n H g * n * g⁻¹ H}, mul_mem' := , one_mem' := , inv_mem' := }
                                                                                                            Instances For
                                                                                                              theorem AddSubgroup.setNormalizer.proof_1 {G : Type u_1} [AddGroup G] (S : Set G) {a : G} {b : G} (ha : ∀ (n : G), n S a + n + -a S) (hb : ∀ (n : G), n S b + n + -b S) (n : G) :
                                                                                                              n S a + b + n + -(a + b) S

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

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                theorem AddSubgroup.setNormalizer.proof_2 {G : Type u_1} [AddGroup G] (S : Set G) (a : G) :
                                                                                                                a S 0 + a + -0 S
                                                                                                                theorem AddSubgroup.setNormalizer.proof_3 {G : Type u_1} [AddGroup G] (S : Set G) {a : G} (ha : ∀ (n : G), n S a + n + -a S) (n : G) :
                                                                                                                n S -a + n + - -a S
                                                                                                                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
                                                                                                                  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 ∀ (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 ∀ (n : G), n + g H g + n 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.le_normalizer {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                                                                                  H H.normalizer
                                                                                                                  theorem Subgroup.le_normalizer {G : Type u_1} [Group G] {H : Subgroup G} :
                                                                                                                  H H.normalizer
                                                                                                                  @[instance 100]
                                                                                                                  instance AddSubgroup.normal_in_normalizer {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                                                                                  (H.addSubgroupOf H.normalizer).Normal
                                                                                                                  Equations
                                                                                                                  • =
                                                                                                                  @[instance 100]
                                                                                                                  instance Subgroup.normal_in_normalizer {G : Type u_1} [Group G] {H : Subgroup G} :
                                                                                                                  (H.subgroupOf H.normalizer).Normal
                                                                                                                  Equations
                                                                                                                  • =
                                                                                                                  theorem AddSubgroup.normalizer_eq_top {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                                                                                                                  H.normalizer = H.Normal
                                                                                                                  theorem Subgroup.normalizer_eq_top {G : Type u_1} [Group G] {H : Subgroup G} :
                                                                                                                  H.normalizer = H.Normal
                                                                                                                  theorem AddSubgroup.le_normalizer_of_normal {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} [hK : (H.addSubgroupOf K).Normal] (HK : H K) :
                                                                                                                  K H.normalizer
                                                                                                                  theorem Subgroup.le_normalizer_of_normal {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [hK : (H.subgroupOf K).Normal] (HK : H K) :
                                                                                                                  K H.normalizer
                                                                                                                  theorem AddSubgroup.le_normalizer_comap {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : Type u_5} [AddGroup N] (f : N →+ G) :
                                                                                                                  AddSubgroup.comap f H.normalizer (AddSubgroup.comap f H).normalizer

                                                                                                                  The preimage of the normalizer is contained in the normalizer of the preimage.

                                                                                                                  theorem Subgroup.le_normalizer_comap {G : Type u_1} [Group G] {H : Subgroup G} {N : Type u_5} [Group N] (f : N →* G) :
                                                                                                                  Subgroup.comap f H.normalizer (Subgroup.comap f H).normalizer

                                                                                                                  The preimage of the normalizer is contained in the normalizer of the preimage.

                                                                                                                  theorem AddSubgroup.le_normalizer_map {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : Type u_5} [AddGroup N] (f : G →+ N) :
                                                                                                                  AddSubgroup.map f H.normalizer (AddSubgroup.map f H).normalizer

                                                                                                                  The image of the normalizer is contained in the normalizer of the image.

                                                                                                                  theorem Subgroup.le_normalizer_map {G : Type u_1} [Group G] {H : Subgroup G} {N : Type u_5} [Group N] (f : G →* N) :
                                                                                                                  Subgroup.map f H.normalizer (Subgroup.map f H).normalizer

                                                                                                                  The image of the normalizer is contained in the normalizer of the image.

                                                                                                                  def NormalizerCondition (G : Type u_1) [Group G] :

                                                                                                                  Every proper subgroup H of G is a proper normal subgroup of the normalizer of H in G.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    theorem normalizerCondition_iff_only_full_group_self_normalizing {G : Type u_1} [Group G] :
                                                                                                                    NormalizerCondition G ∀ (H : Subgroup G), H.normalizer = HH =

                                                                                                                    Alternative phrasing of the normalizer condition: Only the full group is self-normalizing. This may be easier to work with, as it avoids inequalities and negations.

                                                                                                                    class Subgroup.IsCommutative {G : Type u_1} [Group G] (H : Subgroup G) :

                                                                                                                    Commutativity of a subgroup

                                                                                                                    Instances
                                                                                                                      theorem Subgroup.IsCommutative.is_comm {G : Type u_1} [Group G] {H : Subgroup G} (self : H.IsCommutative) :
                                                                                                                      Std.Commutative fun (x1 x2 : { x : G // x H }) => x1 * x2

                                                                                                                      * is commutative on H

                                                                                                                      Commutativity of an additive subgroup

                                                                                                                      Instances
                                                                                                                        theorem AddSubgroup.IsCommutative.is_comm {A : Type u_4} [AddGroup A] {H : AddSubgroup A} (self : H.IsCommutative) :
                                                                                                                        Std.Commutative fun (x1 x2 : { x : A // x H }) => x1 + x2

                                                                                                                        + is commutative on H

                                                                                                                        theorem AddSubgroup.IsCommutative.addCommGroup.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [h : H.IsCommutative] (a : { x : G // x H }) (b : { x : G // x H }) :
                                                                                                                        a + b = b + a
                                                                                                                        instance AddSubgroup.IsCommutative.addCommGroup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [h : H.IsCommutative] :
                                                                                                                        AddCommGroup { x : G // x H }

                                                                                                                        A commutative subgroup is commutative.

                                                                                                                        Equations
                                                                                                                        instance Subgroup.IsCommutative.commGroup {G : Type u_1} [Group G] (H : Subgroup G) [h : H.IsCommutative] :
                                                                                                                        CommGroup { x : G // x H }

                                                                                                                        A commutative subgroup is commutative.

                                                                                                                        Equations
                                                                                                                        instance AddSubgroup.addCommGroup_isCommutative {G : Type u_5} [AddCommGroup G] (H : AddSubgroup G) :
                                                                                                                        H.IsCommutative

                                                                                                                        A subgroup of a commutative group is commutative.

                                                                                                                        Equations
                                                                                                                        • =
                                                                                                                        instance Subgroup.commGroup_isCommutative {G : Type u_5} [CommGroup G] (H : Subgroup G) :
                                                                                                                        H.IsCommutative

                                                                                                                        A subgroup of a commutative group is commutative.

                                                                                                                        Equations
                                                                                                                        • =
                                                                                                                        instance AddSubgroup.map_isCommutative {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') [H.IsCommutative] :
                                                                                                                        (AddSubgroup.map f H).IsCommutative
                                                                                                                        Equations
                                                                                                                        • =
                                                                                                                        instance Subgroup.map_isCommutative {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') [H.IsCommutative] :
                                                                                                                        (Subgroup.map f H).IsCommutative
                                                                                                                        Equations
                                                                                                                        • =
                                                                                                                        theorem AddSubgroup.comap_injective_isCommutative {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G' →+ G} (hf : Function.Injective f) [H.IsCommutative] :
                                                                                                                        (AddSubgroup.comap f H).IsCommutative
                                                                                                                        theorem Subgroup.comap_injective_isCommutative {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G' →* G} (hf : Function.Injective f) [H.IsCommutative] :
                                                                                                                        (Subgroup.comap f H).IsCommutative
                                                                                                                        instance AddSubgroup.addSubgroupOf_isCommutative {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {K : AddSubgroup G} [H.IsCommutative] :
                                                                                                                        (H.addSubgroupOf K).IsCommutative
                                                                                                                        Equations
                                                                                                                        • =
                                                                                                                        instance Subgroup.subgroupOf_isCommutative {G : Type u_1} [Group G] (H : Subgroup G) {K : Subgroup G} [H.IsCommutative] :
                                                                                                                        (H.subgroupOf K).IsCommutative
                                                                                                                        Equations
                                                                                                                        • =
                                                                                                                        theorem AddSubgroup.add_comm_of_mem_isCommutative {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.IsCommutative] {a : G} {b : G} (ha : a H) (hb : b H) :
                                                                                                                        a + b = b + a
                                                                                                                        theorem Subgroup.mul_comm_of_mem_isCommutative {G : Type u_1} [Group G] (H : Subgroup G) [H.IsCommutative] {a : G} {b : G} (ha : a H) (hb : b H) :
                                                                                                                        a * b = b * a
                                                                                                                        @[simp]
                                                                                                                        theorem MulEquiv.comapSubgroup_symm_apply {G : Type u_1} [Group G] {H : Type u_5} [Group H✝] (f : G ≃* H✝) (H : Subgroup G) :
                                                                                                                        (RelIso.symm f.comapSubgroup) H = Subgroup.comap (↑f.symm) H
                                                                                                                        @[simp]
                                                                                                                        theorem MulEquiv.comapSubgroup_apply {G : Type u_1} [Group G] {H : Type u_5} [Group H✝] (f : G ≃* H✝) (H : Subgroup H✝) :
                                                                                                                        f.comapSubgroup H = Subgroup.comap (↑f) H
                                                                                                                        def MulEquiv.comapSubgroup {G : Type u_1} [Group G] {H : Type u_5} [Group H] (f : G ≃* H) :

                                                                                                                        An isomorphism of groups gives an order isomorphism between the lattices of subgroups, defined by sending subgroups to their inverse images.

                                                                                                                        See also MulEquiv.mapSubgroup which maps subgroups to their forward images.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[simp]
                                                                                                                          theorem MulEquiv.mapSubgroup_symm_apply {G : Type u_1} [Group G] {H : Type u_6} [Group H✝] (f : G ≃* H✝) (H : Subgroup H✝) :
                                                                                                                          (RelIso.symm f.mapSubgroup) H = Subgroup.map (↑f.symm) H
                                                                                                                          @[simp]
                                                                                                                          theorem MulEquiv.mapSubgroup_apply {G : Type u_1} [Group G] {H : Type u_6} [Group H✝] (f : G ≃* H✝) (H : Subgroup G) :
                                                                                                                          f.mapSubgroup H = Subgroup.map (↑f) H
                                                                                                                          def MulEquiv.mapSubgroup {G : Type u_1} [Group G] {H : Type u_6} [Group H] (f : G ≃* H) :

                                                                                                                          An isomorphism of groups gives an order isomorphism between the lattices of subgroups, defined by sending subgroups to their forward images.

                                                                                                                          See also MulEquiv.comapSubgroup which maps subgroups to their inverse images.

                                                                                                                          Equations
                                                                                                                          • f.mapSubgroup = { toFun := Subgroup.map f, invFun := Subgroup.map f.symm, left_inv := , right_inv := , map_rel_iff' := }
                                                                                                                          Instances For
                                                                                                                            def Group.conjugatesOfSet {G : Type u_1} [Group G] (s : Set G) :
                                                                                                                            Set G

                                                                                                                            Given a set s, conjugatesOfSet s is the set of all conjugates of the elements of s.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              theorem Group.mem_conjugatesOfSet_iff {G : Type u_1} [Group G] {s : Set G} {x : G} :
                                                                                                                              x Group.conjugatesOfSet s as, IsConj a x
                                                                                                                              theorem Group.conjugates_subset_normal {G : Type u_1} [Group G] {N : Subgroup G} [tn : N.Normal] {a : G} (h : a N) :
                                                                                                                              theorem Group.conjugatesOfSet_subset {G : Type u_1} [Group G] {s : Set G} {N : Subgroup G} [N.Normal] (h : s N) :
                                                                                                                              theorem Group.conj_mem_conjugatesOfSet {G : Type u_1} [Group G] {s : Set G} {x : G} {c : G} :

                                                                                                                              The set of conjugates of s is closed under conjugation.

                                                                                                                              def Subgroup.normalClosure {G : Type u_1} [Group G] (s : Set G) :

                                                                                                                              The normal closure of a set s is the subgroup closure of all the conjugates of elements of s. It is the smallest normal subgroup containing s.

                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                instance Subgroup.normalClosure_normal {G : Type u_1} [Group G] {s : Set G} :

                                                                                                                                The normal closure of s is a normal subgroup.

                                                                                                                                Equations
                                                                                                                                • =
                                                                                                                                theorem Subgroup.normalClosure_le_normal {G : Type u_1} [Group G] {s : Set G} {N : Subgroup G} [N.Normal] (h : s N) :

                                                                                                                                The normal closure of s is the smallest normal subgroup containing s.

                                                                                                                                theorem Subgroup.normalClosure_subset_iff {G : Type u_1} [Group G] {s : Set G} {N : Subgroup G} [N.Normal] :
                                                                                                                                theorem Subgroup.normalClosure_eq_iInf {G : Type u_1} [Group G] {s : Set G} :
                                                                                                                                Subgroup.normalClosure s = ⨅ (N : Subgroup G), ⨅ (_ : N.Normal), ⨅ (_ : s N), N
                                                                                                                                @[simp]
                                                                                                                                theorem Subgroup.normalClosure_eq_self {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] :
                                                                                                                                def Subgroup.normalCore {G : Type u_1} [Group G] (H : Subgroup G) :

                                                                                                                                The normal core of a subgroup H is the largest normal subgroup of G contained in H, as shown by Subgroup.normalCore_eq_iSup.

                                                                                                                                Equations
                                                                                                                                • H.normalCore = { carrier := {a : G | ∀ (b : G), b * a * b⁻¹ H}, mul_mem' := , one_mem' := , inv_mem' := }
                                                                                                                                Instances For
                                                                                                                                  theorem Subgroup.normalCore_le {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                                                                  H.normalCore H
                                                                                                                                  instance Subgroup.normalCore_normal {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                                                                  H.normalCore.Normal
                                                                                                                                  Equations
                                                                                                                                  • =
                                                                                                                                  theorem Subgroup.normal_le_normalCore {G : Type u_1} [Group G] {H : Subgroup G} {N : Subgroup G} [hN : N.Normal] :
                                                                                                                                  N H.normalCore N H
                                                                                                                                  theorem Subgroup.normalCore_mono {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H K) :
                                                                                                                                  H.normalCore K.normalCore
                                                                                                                                  theorem Subgroup.normalCore_eq_iSup {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                                                                  H.normalCore = ⨆ (N : Subgroup G), ⨆ (_ : N.Normal), ⨆ (_ : N H), N
                                                                                                                                  @[simp]
                                                                                                                                  theorem Subgroup.normalCore_eq_self {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] :
                                                                                                                                  H.normalCore = H
                                                                                                                                  theorem Subgroup.normalCore_idempotent {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                                                                  H.normalCore.normalCore = H.normalCore
                                                                                                                                  def AddMonoidHom.range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :

                                                                                                                                  The range of an AddMonoidHom from an AddGroup is an AddSubgroup.

                                                                                                                                  Equations
                                                                                                                                  Instances For
                                                                                                                                    theorem AddMonoidHom.range.proof_1 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] (f : G →+ N) :
                                                                                                                                    Set.range f = f '' Set.univ
                                                                                                                                    def MonoidHom.range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :

                                                                                                                                    The range of a monoid homomorphism from a group is a subgroup.

                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      @[simp]
                                                                                                                                      theorem AddMonoidHom.coe_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                                                                                                                                      f.range = Set.range f
                                                                                                                                      @[simp]
                                                                                                                                      theorem MonoidHom.coe_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                                                                                                                                      f.range = Set.range f
                                                                                                                                      @[simp]
                                                                                                                                      theorem AddMonoidHom.mem_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {y : N} :
                                                                                                                                      y f.range ∃ (x : G), f x = y
                                                                                                                                      @[simp]
                                                                                                                                      theorem MonoidHom.mem_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {y : N} :
                                                                                                                                      y f.range ∃ (x : G), f x = y
                                                                                                                                      theorem AddMonoidHom.range_eq_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                                                                                                                                      theorem MonoidHom.range_eq_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                                                                                                                                      f.range = Subgroup.map f
                                                                                                                                      instance AddMonoidHom.range_isCommutative {G : Type u_7} [AddCommGroup G] {N : Type u_8} [AddGroup N] (f : G →+ N) :
                                                                                                                                      f.range.IsCommutative
                                                                                                                                      Equations
                                                                                                                                      • =
                                                                                                                                      instance MonoidHom.range_isCommutative {G : Type u_7} [CommGroup G] {N : Type u_8} [Group N] (f : G →* N) :
                                                                                                                                      f.range.IsCommutative
                                                                                                                                      Equations
                                                                                                                                      • =
                                                                                                                                      @[simp]
                                                                                                                                      theorem AddMonoidHom.restrict_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) (f : G →+ N) :
                                                                                                                                      (f.restrict K).range = AddSubgroup.map f K
                                                                                                                                      @[simp]
                                                                                                                                      theorem MonoidHom.restrict_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) (f : G →* N) :
                                                                                                                                      (f.restrict K).range = Subgroup.map f K
                                                                                                                                      theorem AddMonoidHom.rangeRestrict.proof_2 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (f : G →+ N) (x : G) :
                                                                                                                                      ∃ (y : G), f y = f x
                                                                                                                                      def AddMonoidHom.rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                                                                                                                                      G →+ { x : N // x f.range }

                                                                                                                                      The canonical surjective AddGroup homomorphism G →+ f(G) induced by a group homomorphism G →+ N.

                                                                                                                                      Equations
                                                                                                                                      • f.rangeRestrict = f.codRestrict f.range
                                                                                                                                      Instances For
                                                                                                                                        def MonoidHom.rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                                                                                                                                        G →* { x : N // x f.range }

                                                                                                                                        The canonical surjective group homomorphism G →* f(G) induced by a group homomorphism G →* N.

                                                                                                                                        Equations
                                                                                                                                        • f.rangeRestrict = f.codRestrict f.range
                                                                                                                                        Instances For
                                                                                                                                          @[simp]
                                                                                                                                          theorem AddMonoidHom.coe_rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (g : G) :
                                                                                                                                          (f.rangeRestrict g) = f g
                                                                                                                                          @[simp]
                                                                                                                                          theorem MonoidHom.coe_rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (g : G) :
                                                                                                                                          (f.rangeRestrict g) = f g
                                                                                                                                          theorem AddMonoidHom.coe_comp_rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                                                                                                                                          Subtype.val f.rangeRestrict = f
                                                                                                                                          theorem MonoidHom.coe_comp_rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                                                                                                                                          Subtype.val f.rangeRestrict = f
                                                                                                                                          theorem AddMonoidHom.subtype_comp_rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                                                                                                                                          f.range.subtype.comp f.rangeRestrict = f
                                                                                                                                          theorem MonoidHom.subtype_comp_rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                                                                                                                                          f.range.subtype.comp f.rangeRestrict = f
                                                                                                                                          theorem AddMonoidHom.rangeRestrict_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                                                                                                                                          Function.Surjective f.rangeRestrict
                                                                                                                                          theorem MonoidHom.rangeRestrict_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                                                                                                                                          Function.Surjective f.rangeRestrict
                                                                                                                                          @[simp]
                                                                                                                                          theorem AddMonoidHom.rangeRestrict_injective_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} :
                                                                                                                                          Function.Injective f.rangeRestrict Function.Injective f
                                                                                                                                          @[simp]
                                                                                                                                          theorem MonoidHom.rangeRestrict_injective_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} :
                                                                                                                                          Function.Injective f.rangeRestrict Function.Injective f
                                                                                                                                          theorem AddMonoidHom.map_range {G : Type u_1} [AddGroup G] {N : Type u_5} {P : Type u_6} [AddGroup N] [AddGroup P] (g : N →+ P) (f : G →+ N) :
                                                                                                                                          AddSubgroup.map g f.range = (g.comp f).range
                                                                                                                                          theorem MonoidHom.map_range {G : Type u_1} [Group G] {N : Type u_5} {P : Type u_6} [Group N] [Group P] (g : N →* P) (f : G →* N) :
                                                                                                                                          Subgroup.map g f.range = (g.comp f).range
                                                                                                                                          theorem AddMonoidHom.range_top_iff_surjective {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] {f : G →+ N} :
                                                                                                                                          theorem MonoidHom.range_top_iff_surjective {G : Type u_1} [Group G] {N : Type u_7} [Group N] {f : G →* N} :
                                                                                                                                          @[simp]
                                                                                                                                          theorem AddMonoidHom.range_top_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] (f : G →+ N) (hf : Function.Surjective f) :
                                                                                                                                          f.range =

                                                                                                                                          The range of a surjective AddMonoid homomorphism is the whole of the codomain.

                                                                                                                                          @[simp]
                                                                                                                                          theorem MonoidHom.range_top_of_surjective {G : Type u_1} [Group G] {N : Type u_7} [Group N] (f : G →* N) (hf : Function.Surjective f) :
                                                                                                                                          f.range =

                                                                                                                                          The range of a surjective monoid homomorphism is the whole of the codomain.

                                                                                                                                          @[simp]
                                                                                                                                          theorem AddMonoidHom.range_zero {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] :
                                                                                                                                          @[simp]
                                                                                                                                          theorem MonoidHom.range_one {G : Type u_1} [Group G] {N : Type u_5} [Group N] :
                                                                                                                                          @[simp]
                                                                                                                                          theorem AddSubgroup.subtype_range {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                                                                                                          H.subtype.range = H
                                                                                                                                          @[simp]
                                                                                                                                          theorem Subgroup.subtype_range {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                                                                          H.subtype.range = H
                                                                                                                                          @[simp]
                                                                                                                                          theorem AddSubgroup.inclusion_range {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h_le : H K) :
                                                                                                                                          (AddSubgroup.inclusion h_le).range = H.addSubgroupOf K
                                                                                                                                          @[simp]
                                                                                                                                          theorem Subgroup.inclusion_range {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h_le : H K) :
                                                                                                                                          (Subgroup.inclusion h_le).range = H.subgroupOf K
                                                                                                                                          theorem AddMonoidHom.addSubgroupOf_range_eq_of_le {G₁ : Type u_7} {G₂ : Type u_8} [AddGroup G₁] [AddGroup G₂] {K : AddSubgroup G₂} (f : G₁ →+ G₂) (h : f.range K) :
                                                                                                                                          f.range.addSubgroupOf K = (f.codRestrict K ).range
                                                                                                                                          theorem MonoidHom.subgroupOf_range_eq_of_le {G₁ : Type u_7} {G₂ : Type u_8} [Group G₁] [Group G₂] {K : Subgroup G₂} (f : G₁ →* G₂) (h : f.range K) :
                                                                                                                                          f.range.subgroupOf K = (f.codRestrict K ).range
                                                                                                                                          @[simp]
                                                                                                                                          theorem MonoidHom.coe_toAdditive_range {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') :
                                                                                                                                          (MonoidHom.toAdditive f).range = Subgroup.toAddSubgroup f.range
                                                                                                                                          @[simp]
                                                                                                                                          theorem MonoidHom.coe_toMultiplicative_range {A : Type u_7} {A' : Type u_8} [AddGroup A] [AddGroup A'] (f : A →+ A') :
                                                                                                                                          (AddMonoidHom.toMultiplicative f).range = AddSubgroup.toSubgroup f.range
                                                                                                                                          theorem AddMonoidHom.ofLeftInverse.proof_1 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse g f) :
                                                                                                                                          ∀ (x : { x : N // x f.range }), f.rangeRestrict ((g f.range.subtype) x) = x
                                                                                                                                          def AddMonoidHom.ofLeftInverse {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse g f) :
                                                                                                                                          G ≃+ { x : N // x f.range }

                                                                                                                                          Computable alternative to AddMonoidHom.ofInjective.

                                                                                                                                          Equations
                                                                                                                                          • AddMonoidHom.ofLeftInverse h = { toFun := f.rangeRestrict, invFun := g f.range.subtype, left_inv := h, right_inv := , map_add' := }
                                                                                                                                          Instances For
                                                                                                                                            theorem AddMonoidHom.ofLeftInverse.proof_2 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] {f : G →+ N} (x : G) (y : G) :
                                                                                                                                            (↑f.rangeRestrict).toFun (x + y) = (↑f.rangeRestrict).toFun x + (↑f.rangeRestrict).toFun y
                                                                                                                                            def MonoidHom.ofLeftInverse {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) :
                                                                                                                                            G ≃* { x : N // x f.range }

                                                                                                                                            Computable alternative to MonoidHom.ofInjective.

                                                                                                                                            Equations
                                                                                                                                            • MonoidHom.ofLeftInverse h = { toFun := f.rangeRestrict, invFun := g f.range.subtype, left_inv := h, right_inv := , map_mul' := }
                                                                                                                                            Instances For
                                                                                                                                              @[simp]
                                                                                                                                              theorem AddMonoidHom.ofLeftInverse_apply {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse g f) (x : G) :
                                                                                                                                              @[simp]
                                                                                                                                              theorem MonoidHom.ofLeftInverse_apply {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) (x : G) :
                                                                                                                                              ((MonoidHom.ofLeftInverse h) x) = f x
                                                                                                                                              @[simp]
                                                                                                                                              theorem AddMonoidHom.ofLeftInverse_symm_apply {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse g f) (x : { x : N // x f.range }) :
                                                                                                                                              (AddMonoidHom.ofLeftInverse h).symm x = g x
                                                                                                                                              @[simp]
                                                                                                                                              theorem MonoidHom.ofLeftInverse_symm_apply {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (h : Function.LeftInverse g f) (x : { x : N // x f.range }) :
                                                                                                                                              (MonoidHom.ofLeftInverse h).symm x = g x
                                                                                                                                              theorem AddMonoidHom.ofInjective.proof_4 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] {f : G →+ N} (hf : Function.Injective f) :
                                                                                                                                              Function.Injective (f.codRestrict f.range ) Function.Surjective (f.codRestrict f.range )
                                                                                                                                              theorem AddMonoidHom.ofInjective.proof_3 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] {f : G →+ N} (x : G) :
                                                                                                                                              ∃ (y : G), f y = f x
                                                                                                                                              theorem AddMonoidHom.ofInjective.proof_2 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] {f : G →+ N} :
                                                                                                                                              AddHomClass (G →+ { x : N // x f.range }) G { x : N // x f.range }
                                                                                                                                              noncomputable def AddMonoidHom.ofInjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective f) :
                                                                                                                                              G ≃+ { x : N // x f.range }

                                                                                                                                              The range of an injective additive group homomorphism is isomorphic to its domain.

                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                noncomputable def MonoidHom.ofInjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective f) :
                                                                                                                                                G ≃* { x : N // x f.range }

                                                                                                                                                The range of an injective group homomorphism is isomorphic to its domain.

                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  theorem AddMonoidHom.ofInjective_apply {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective f) {x : G} :
                                                                                                                                                  ((AddMonoidHom.ofInjective hf) x) = f x
                                                                                                                                                  theorem MonoidHom.ofInjective_apply {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective f) {x : G} :
                                                                                                                                                  ((MonoidHom.ofInjective hf) x) = f x
                                                                                                                                                  @[simp]
                                                                                                                                                  theorem AddMonoidHom.apply_ofInjective_symm {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective f) (x : { x : N // x f.range }) :
                                                                                                                                                  f ((AddMonoidHom.ofInjective hf).symm x) = x
                                                                                                                                                  @[simp]
                                                                                                                                                  theorem MonoidHom.apply_ofInjective_symm {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective f) (x : { x : N // x f.range }) :
                                                                                                                                                  f ((MonoidHom.ofInjective hf).symm x) = x
                                                                                                                                                  def AddMonoidHom.ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) :

                                                                                                                                                  The additive kernel of an AddMonoid homomorphism is the AddSubgroup of elements such that f x = 0

                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    theorem AddMonoidHom.ker.proof_1 {G : Type u_2} [AddGroup G] {M : Type u_1} [AddZeroClass M] :
                                                                                                                                                    theorem AddMonoidHom.ker.proof_2 {G : Type u_2} [AddGroup G] {M : Type u_1} [AddZeroClass M] (f : G →+ M) {x : G} (hx : f x = 0) :
                                                                                                                                                    f (-x) = 0
                                                                                                                                                    def MonoidHom.ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) :

                                                                                                                                                    The multiplicative kernel of a monoid homomorphism is the subgroup of elements x : G such that f x = 1

                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      theorem AddMonoidHom.mem_ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) {x : G} :
                                                                                                                                                      x f.ker f x = 0
                                                                                                                                                      theorem MonoidHom.mem_ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) {x : G} :
                                                                                                                                                      x f.ker f x = 1
                                                                                                                                                      theorem AddMonoidHom.sub_mem_ker_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {x : G} {y : G} :
                                                                                                                                                      x - y f.ker f x = f y
                                                                                                                                                      theorem MonoidHom.div_mem_ker_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {x : G} {y : G} :
                                                                                                                                                      x / y f.ker f x = f y
                                                                                                                                                      theorem AddMonoidHom.coe_ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) :
                                                                                                                                                      f.ker = f ⁻¹' {0}
                                                                                                                                                      theorem MonoidHom.coe_ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) :
                                                                                                                                                      f.ker = f ⁻¹' {1}
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem AddMonoidHom.ker_toHomAddUnits {G : Type u_1} [AddGroup G] {M : Type u_8} [AddMonoid M] (f : G →+ M) :
                                                                                                                                                      f.toHomAddUnits.ker = f.ker
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem MonoidHom.ker_toHomUnits {G : Type u_1} [Group G] {M : Type u_8} [Monoid M] (f : G →* M) :
                                                                                                                                                      f.toHomUnits.ker = f.ker
                                                                                                                                                      theorem AddMonoidHom.eq_iff {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) {x : G} {y : G} :
                                                                                                                                                      f x = f y -y + x f.ker
                                                                                                                                                      theorem MonoidHom.eq_iff {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) {x : G} {y : G} :
                                                                                                                                                      f x = f y y⁻¹ * x f.ker
                                                                                                                                                      instance AddMonoidHom.decidableMemKer {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] [DecidableEq M] (f : G →+ M) :
                                                                                                                                                      DecidablePred fun (x : G) => x f.ker
                                                                                                                                                      Equations
                                                                                                                                                      instance MonoidHom.decidableMemKer {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] [DecidableEq M] (f : G →* M) :
                                                                                                                                                      DecidablePred fun (x : G) => x f.ker
                                                                                                                                                      Equations
                                                                                                                                                      theorem AddMonoidHom.comap_ker {G : Type u_1} [AddGroup G] {N : Type u_5} {P : Type u_6} [AddGroup N] [AddGroup P] (g : N →+ P) (f : G →+ N) :
                                                                                                                                                      AddSubgroup.comap f g.ker = (g.comp f).ker
                                                                                                                                                      theorem MonoidHom.comap_ker {G : Type u_1} [Group G] {N : Type u_5} {P : Type u_6} [Group N] [Group P] (g : N →* P) (f : G →* N) :
                                                                                                                                                      Subgroup.comap f g.ker = (g.comp f).ker
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem AddMonoidHom.comap_bot {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem MonoidHom.comap_bot {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem AddMonoidHom.ker_restrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) (f : G →+ N) :
                                                                                                                                                      (f.restrict K).ker = f.ker.addSubgroupOf K
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem MonoidHom.ker_restrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) (f : G →* N) :
                                                                                                                                                      (f.restrict K).ker = f.ker.subgroupOf K
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem AddMonoidHom.ker_codRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {S : Type u_8} [SetLike S N] [AddSubmonoidClass S N] (f : G →+ N) (s : S) (h : ∀ (x : G), f x s) :
                                                                                                                                                      (f.codRestrict s h).ker = f.ker
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem MonoidHom.ker_codRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] {S : Type u_8} [SetLike S N] [SubmonoidClass S N] (f : G →* N) (s : S) (h : ∀ (x : G), f x s) :
                                                                                                                                                      (f.codRestrict s h).ker = f.ker
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem AddMonoidHom.ker_rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                                                                                                                                                      f.rangeRestrict.ker = f.ker
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem MonoidHom.ker_rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                                                                                                                                                      f.rangeRestrict.ker = f.ker
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem AddMonoidHom.ker_zero {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] :
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem MonoidHom.ker_one {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] :
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem AddMonoidHom.ker_id {G : Type u_1} [AddGroup G] :
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem MonoidHom.ker_id {G : Type u_1} [Group G] :
                                                                                                                                                      theorem AddMonoidHom.ker_eq_bot_iff {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) :
                                                                                                                                                      theorem MonoidHom.ker_eq_bot_iff {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) :
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem AddSubgroup.ker_subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
                                                                                                                                                      H.subtype.ker =
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem Subgroup.ker_subtype {G : Type u_1} [Group G] (H : Subgroup G) :
                                                                                                                                                      H.subtype.ker =
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem AddSubgroup.ker_inclusion {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H K) :
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem Subgroup.ker_inclusion {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H K) :
                                                                                                                                                      theorem AddMonoidHom.ker_sum {G : Type u_1} [AddGroup G] {M : Type u_8} {N : Type u_9} [AddZeroClass M] [AddZeroClass N] (f : G →+ M) (g : G →+ N) :
                                                                                                                                                      (f.prod g).ker = f.ker g.ker
                                                                                                                                                      theorem MonoidHom.ker_prod {G : Type u_1} [Group G] {M : Type u_8} {N : Type u_9} [MulOneClass M] [MulOneClass N] (f : G →* M) (g : G →* N) :
                                                                                                                                                      (f.prod g).ker = f.ker g.ker
                                                                                                                                                      theorem AddMonoidHom.sumMap_comap_sum {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {G' : Type u_8} {N' : Type u_9} [AddGroup G'] [AddGroup N'] (f : G →+ N) (g : G' →+ N') (S : AddSubgroup N) (S' : AddSubgroup N') :
                                                                                                                                                      AddSubgroup.comap (f.prodMap g) (S.prod S') = (AddSubgroup.comap f S).prod (AddSubgroup.comap g S')
                                                                                                                                                      theorem MonoidHom.prodMap_comap_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] {G' : Type u_8} {N' : Type u_9} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') (S : Subgroup N) (S' : Subgroup N') :
                                                                                                                                                      Subgroup.comap (f.prodMap g) (S.prod S') = (Subgroup.comap f S).prod (Subgroup.comap g S')
                                                                                                                                                      theorem AddMonoidHom.ker_sumMap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {G' : Type u_8} {N' : Type u_9} [AddGroup G'] [AddGroup N'] (f : G →+ N) (g : G' →+ N') :
                                                                                                                                                      (f.prodMap g).ker = f.ker.prod g.ker
                                                                                                                                                      theorem MonoidHom.ker_prodMap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {G' : Type u_8} {N' : Type u_9} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') :
                                                                                                                                                      (f.prodMap g).ker = f.ker.prod g.ker
                                                                                                                                                      theorem AddMonoidHom.range_le_ker_iff {G : Type u_1} {G' : Type u_2} {G'' : Type u_3} [AddGroup G] [AddGroup G'] [AddGroup G''] (f : G →+ G') (g : G' →+ G'') :
                                                                                                                                                      f.range g.ker g.comp f = 0
                                                                                                                                                      theorem MonoidHom.range_le_ker_iff {G : Type u_1} {G' : Type u_2} {G'' : Type u_3} [Group G] [Group G'] [Group G''] (f : G →* G') (g : G' →* G'') :
                                                                                                                                                      f.range g.ker g.comp f = 1
                                                                                                                                                      @[instance 100]
                                                                                                                                                      instance AddMonoidHom.normal_ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) :
                                                                                                                                                      f.ker.Normal
                                                                                                                                                      Equations
                                                                                                                                                      • =
                                                                                                                                                      @[instance 100]
                                                                                                                                                      instance MonoidHom.normal_ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) :
                                                                                                                                                      f.ker.Normal
                                                                                                                                                      Equations
                                                                                                                                                      • =
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem AddMonoidHom.ker_fst {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] :
                                                                                                                                                      (AddMonoidHom.fst G G').ker = .prod
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem MonoidHom.ker_fst {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] :
                                                                                                                                                      (MonoidHom.fst G G').ker = .prod
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem AddMonoidHom.ker_snd {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] :
                                                                                                                                                      (AddMonoidHom.snd G G').ker = .prod
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem MonoidHom.ker_snd {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] :
                                                                                                                                                      (MonoidHom.snd G G').ker = .prod
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem MonoidHom.coe_toAdditive_ker {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') :
                                                                                                                                                      (MonoidHom.toAdditive f).ker = Subgroup.toAddSubgroup f.ker
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem MonoidHom.coe_toMultiplicative_ker {A : Type u_8} {A' : Type u_9} [AddGroup A] [AddGroup A'] (f : A →+ A') :
                                                                                                                                                      (AddMonoidHom.toMultiplicative f).ker = AddSubgroup.toSubgroup f.ker
                                                                                                                                                      theorem AddMonoidHom.eqLocus.proof_1 {G : Type u_2} [AddGroup G] {M : Type u_1} [AddMonoid M] (f : G →+ M) (g : G →+ M) :
                                                                                                                                                      ∀ {x : G}, f x = g xf (-x) = g (-x)
                                                                                                                                                      def AddMonoidHom.eqLocus {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] (f : G →+ M) (g : G →+ M) :

                                                                                                                                                      The additive subgroup of elements x : G such that f x = g x

                                                                                                                                                      Equations
                                                                                                                                                      • f.eqLocus g = { toAddSubmonoid := f.eqLocusM g, neg_mem' := }
                                                                                                                                                      Instances For
                                                                                                                                                        def MonoidHom.eqLocus {G : Type u_1} [Group G] {M : Type u_7} [Monoid M] (f : G →* M) (g : G →* M) :

                                                                                                                                                        The subgroup of elements x : G such that f x = g x

                                                                                                                                                        Equations
                                                                                                                                                        • f.eqLocus g = { toSubmonoid := f.eqLocusM g, inv_mem' := }
                                                                                                                                                        Instances For
                                                                                                                                                          @[simp]
                                                                                                                                                          theorem AddMonoidHom.eqLocus_same {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                                                                                                                                                          f.eqLocus f =
                                                                                                                                                          @[simp]
                                                                                                                                                          theorem MonoidHom.eqLocus_same {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                                                                                                                                                          f.eqLocus f =
                                                                                                                                                          theorem AddMonoidHom.eqOn_closure {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] {f : G →+ M} {g : G →+ M} {s : Set G} (h : Set.EqOn (⇑f) (⇑g) s) :
                                                                                                                                                          Set.EqOn f g (AddSubgroup.closure s)

                                                                                                                                                          If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure.

                                                                                                                                                          theorem MonoidHom.eqOn_closure {G : Type u_1} [Group G] {M : Type u_7} [Monoid M] {f : G →* M} {g : G →* M} {s : Set G} (h : Set.EqOn (⇑f) (⇑g) s) :
                                                                                                                                                          Set.EqOn f g (Subgroup.closure s)

                                                                                                                                                          If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure.

                                                                                                                                                          theorem AddMonoidHom.eq_of_eqOn_top {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] {f : G →+ M} {g : G →+ M} (h : Set.EqOn f g ) :
                                                                                                                                                          f = g
                                                                                                                                                          theorem MonoidHom.eq_of_eqOn_top {G : Type u_1} [Group G] {M : Type u_7} [Monoid M] {f : G →* M} {g : G →* M} (h : Set.EqOn f g ) :
                                                                                                                                                          f = g
                                                                                                                                                          theorem AddMonoidHom.eq_of_eqOn_dense {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] {s : Set G} (hs : AddSubgroup.closure s = ) {f : G →+ M} {g : G →+ M} (h : Set.EqOn (⇑f) (⇑g) s) :
                                                                                                                                                          f = g
                                                                                                                                                          theorem MonoidHom.eq_of_eqOn_dense {G : Type u_1} [Group G] {M : Type u_7} [Monoid M] {s : Set G} (hs : Subgroup.closure s = ) {f : G →* M} {g : G →* M} (h : Set.EqOn (⇑f) (⇑g) s) :
                                                                                                                                                          f = g
                                                                                                                                                          theorem MonoidHom.closure_preimage_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (s : Set N) :
                                                                                                                                                          theorem AddMonoidHom.map_closure {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (s : Set G) :

                                                                                                                                                          The image under an AddMonoid hom of the AddSubgroup generated by a set equals the AddSubgroup generated by the image of the set.

                                                                                                                                                          theorem MonoidHom.map_closure {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (s : Set G) :

                                                                                                                                                          The image under a monoid homomorphism of the subgroup generated by a set equals the subgroup generated by the image of the set.

                                                                                                                                                          theorem AddSubgroup.Normal.map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} (h : H.Normal) (f : G →+ N) (hf : Function.Surjective f) :
                                                                                                                                                          (AddSubgroup.map f H).Normal
                                                                                                                                                          theorem Subgroup.Normal.map {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} (h : H.Normal) (f : G →* N) (hf : Function.Surjective f) :
                                                                                                                                                          (Subgroup.map f H).Normal
                                                                                                                                                          theorem AddSubgroup.map_eq_bot_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} :
                                                                                                                                                          theorem Subgroup.map_eq_bot_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : G →* N} :
                                                                                                                                                          Subgroup.map f H = H f.ker
                                                                                                                                                          theorem AddSubgroup.map_eq_bot_iff_of_injective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} (hf : Function.Injective f) :
                                                                                                                                                          theorem Subgroup.map_eq_bot_iff_of_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : G →* N} (hf : Function.Injective f) :
                                                                                                                                                          theorem AddSubgroup.map_le_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) :
                                                                                                                                                          AddSubgroup.map f H f.range
                                                                                                                                                          theorem Subgroup.map_le_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) :
                                                                                                                                                          Subgroup.map f H f.range
                                                                                                                                                          theorem AddSubgroup.map_subtype_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (K : AddSubgroup { x : G // x H }) :
                                                                                                                                                          AddSubgroup.map H.subtype K H
                                                                                                                                                          theorem Subgroup.map_subtype_le {G : Type u_1} [Group G] {H : Subgroup G} (K : Subgroup { x : G // x H }) :
                                                                                                                                                          Subgroup.map H.subtype K H
                                                                                                                                                          theorem AddSubgroup.ker_le_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) :
                                                                                                                                                          theorem Subgroup.ker_le_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) :
                                                                                                                                                          theorem AddSubgroup.map_comap_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) :
                                                                                                                                                          theorem Subgroup.map_comap_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) :
                                                                                                                                                          theorem AddSubgroup.le_comap_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) :
                                                                                                                                                          theorem Subgroup.le_comap_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) :
                                                                                                                                                          theorem AddSubgroup.map_comap_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) :
                                                                                                                                                          theorem Subgroup.map_comap_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) :
                                                                                                                                                          Subgroup.map f (Subgroup.comap f H) = f.range H
                                                                                                                                                          theorem AddSubgroup.comap_map_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) :
                                                                                                                                                          theorem Subgroup.comap_map_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) :
                                                                                                                                                          theorem AddSubgroup.map_comap_eq_self {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup N} (h : H f.range) :
                                                                                                                                                          theorem Subgroup.map_comap_eq_self {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup N} (h : H f.range) :
                                                                                                                                                          theorem Subgroup.map_comap_eq_self_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Surjective f) (H : Subgroup N) :
                                                                                                                                                          theorem AddSubgroup.comap_le_comap_of_le_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup N} {L : AddSubgroup N} (hf : K f.range) :
                                                                                                                                                          theorem Subgroup.comap_le_comap_of_le_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup N} {L : Subgroup N} (hf : K f.range) :
                                                                                                                                                          theorem Subgroup.comap_le_comap_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup N} {L : Subgroup N} (hf : Function.Surjective f) :
                                                                                                                                                          theorem Subgroup.comap_lt_comap_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup N} {L : Subgroup N} (hf : Function.Surjective f) :
                                                                                                                                                          theorem Subgroup.comap_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Surjective f) :
                                                                                                                                                          theorem AddSubgroup.comap_map_eq_self {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} (h : f.ker H) :
                                                                                                                                                          theorem Subgroup.comap_map_eq_self {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} (h : f.ker H) :
                                                                                                                                                          theorem Subgroup.comap_map_eq_self_of_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Injective f) (H : Subgroup G) :
                                                                                                                                                          theorem AddSubgroup.map_le_map_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} {K : AddSubgroup G} :
                                                                                                                                                          theorem Subgroup.map_le_map_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} {K : Subgroup G} :
                                                                                                                                                          theorem AddSubgroup.map_le_map_iff' {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} {K : AddSubgroup G} :
                                                                                                                                                          AddSubgroup.map f H AddSubgroup.map f K H f.ker K f.ker
                                                                                                                                                          theorem Subgroup.map_le_map_iff' {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} {K : Subgroup G} :
                                                                                                                                                          Subgroup.map f H Subgroup.map f K H f.ker K f.ker
                                                                                                                                                          theorem AddSubgroup.map_eq_map_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} {K : AddSubgroup G} :
                                                                                                                                                          AddSubgroup.map f H = AddSubgroup.map f K H f.ker = K f.ker
                                                                                                                                                          theorem Subgroup.map_eq_map_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} {K : Subgroup G} :
                                                                                                                                                          Subgroup.map f H = Subgroup.map f K H f.ker = K f.ker
                                                                                                                                                          theorem AddSubgroup.map_eq_range_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} :
                                                                                                                                                          AddSubgroup.map f H = f.range Codisjoint H f.ker
                                                                                                                                                          theorem Subgroup.map_eq_range_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} :
                                                                                                                                                          Subgroup.map f H = f.range Codisjoint H f.ker
                                                                                                                                                          theorem Subgroup.map_le_map_iff_of_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective f) {H : Subgroup G} {K : Subgroup G} :
                                                                                                                                                          @[simp]
                                                                                                                                                          theorem AddSubgroup.map_subtype_le_map_subtype {G : Type u_1} [AddGroup G] {G' : AddSubgroup G} {H : AddSubgroup { x : G // x G' }} {K : AddSubgroup { x : G // x G' }} :
                                                                                                                                                          AddSubgroup.map G'.subtype H AddSubgroup.map G'.subtype K H K
                                                                                                                                                          @[simp]
                                                                                                                                                          theorem Subgroup.map_subtype_le_map_subtype {G : Type u_1} [Group G] {G' : Subgroup G} {H : Subgroup { x : G // x G' }} {K : Subgroup { x : G // x G' }} :
                                                                                                                                                          Subgroup.map G'.subtype H Subgroup.map G'.subtype K H K
                                                                                                                                                          theorem Subgroup.map_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Injective f) :
                                                                                                                                                          theorem AddSubgroup.map_eq_comap_of_inverse {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (hl : Function.LeftInverse g f) (hr : Function.RightInverse g f) (H : AddSubgroup G) :
                                                                                                                                                          theorem Subgroup.map_eq_comap_of_inverse {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (hl : Function.LeftInverse g f) (hr : Function.RightInverse g f) (H : Subgroup G) :
                                                                                                                                                          theorem AddSubgroup.map_injective_of_ker_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {H : AddSubgroup G} {K : AddSubgroup G} (hH : f.ker H) (hK : f.ker K) (hf : AddSubgroup.map f H = AddSubgroup.map f K) :
                                                                                                                                                          H = K

                                                                                                                                                          Given f(A) = f(B), ker f ≤ A, and ker f ≤ B, deduce that A = B.

                                                                                                                                                          theorem Subgroup.map_injective_of_ker_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {H : Subgroup G} {K : Subgroup G} (hH : f.ker H) (hK : f.ker K) (hf : Subgroup.map f H = Subgroup.map f K) :
                                                                                                                                                          H = K

                                                                                                                                                          Given f(A) = f(B), ker f ≤ A, and ker f ≤ B, deduce that A = B.

                                                                                                                                                          theorem AddSubgroup.comap_sup_eq_of_le_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {H : AddSubgroup N} {K : AddSubgroup N} (hH : H f.range) (hK : K f.range) :
                                                                                                                                                          theorem Subgroup.comap_sup_eq_of_le_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {H : Subgroup N} {K : Subgroup N} (hH : H f.range) (hK : K f.range) :
                                                                                                                                                          theorem AddSubgroup.comap_sup_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) (K : AddSubgroup N) (hf : Function.Surjective f) :
                                                                                                                                                          theorem Subgroup.comap_sup_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) (K : Subgroup N) (hf : Function.Surjective f) :
                                                                                                                                                          theorem AddSubgroup.sup_addSubgroupOf_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {L : AddSubgroup G} (hH : H L) (hK : K L) :
                                                                                                                                                          H.addSubgroupOf L K.addSubgroupOf L = (H K).addSubgroupOf L
                                                                                                                                                          theorem Subgroup.sup_subgroupOf_eq {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hH : H L) (hK : K L) :
                                                                                                                                                          H.subgroupOf L K.subgroupOf L = (H K).subgroupOf L
                                                                                                                                                          theorem AddSubgroup.codisjoint_addSubgroupOf_sup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) :
                                                                                                                                                          Codisjoint (H.addSubgroupOf (H K)) (K.addSubgroupOf (H K))
                                                                                                                                                          theorem Subgroup.codisjoint_subgroupOf_sup {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) :
                                                                                                                                                          Codisjoint (H.subgroupOf (H K)) (K.subgroupOf (H K))
                                                                                                                                                          noncomputable def AddSubgroup.equivMapOfInjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective f) :
                                                                                                                                                          { x : G // x H } ≃+ { x : N // x AddSubgroup.map f H }

                                                                                                                                                          An additive subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use AddEquiv.addSubgroupMap for better definitional equalities.

                                                                                                                                                          Equations
                                                                                                                                                          • H.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_add' := }
                                                                                                                                                          Instances For
                                                                                                                                                            theorem AddSubgroup.equivMapOfInjective.proof_1 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective f) :
                                                                                                                                                            ∀ (x x_1 : { x : G // x H }), (Equiv.Set.image (⇑f) (↑H) hf).toFun (x + x_1) = (Equiv.Set.image (⇑f) (↑H) hf).toFun x + (Equiv.Set.image (⇑f) (↑H) hf).toFun x_1
                                                                                                                                                            noncomputable def Subgroup.equivMapOfInjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
                                                                                                                                                            { x : G // x H } ≃* { x : N // x Subgroup.map f H }

                                                                                                                                                            A subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use MulEquiv.subgroupMap for better definitional equalities.

                                                                                                                                                            Equations
                                                                                                                                                            • H.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_mul' := }
                                                                                                                                                            Instances For
                                                                                                                                                              @[simp]
                                                                                                                                                              theorem AddSubgroup.coe_equivMapOfInjective_apply {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective f) (h : { x : G // x H }) :
                                                                                                                                                              ((H.equivMapOfInjective f hf) h) = f h
                                                                                                                                                              @[simp]
                                                                                                                                                              theorem Subgroup.coe_equivMapOfInjective_apply {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G →* N) (hf : Function.Injective f) (h : { x : G // x H }) :
                                                                                                                                                              ((H.equivMapOfInjective f hf) h) = f h
                                                                                                                                                              theorem AddSubgroup.comap_normalizer_eq_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : N →+ G} (hf : Function.Surjective f) :
                                                                                                                                                              AddSubgroup.comap f H.normalizer = (AddSubgroup.comap f H).normalizer

                                                                                                                                                              The preimage of the normalizer is equal to the normalizer of the preimage of a surjective function.

                                                                                                                                                              theorem Subgroup.comap_normalizer_eq_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : N →* G} (hf : Function.Surjective f) :
                                                                                                                                                              Subgroup.comap f H.normalizer = (Subgroup.comap f H).normalizer

                                                                                                                                                              The preimage of the normalizer is equal to the normalizer of the preimage of a surjective function.

                                                                                                                                                              theorem AddSubgroup.comap_normalizer_eq_of_injective_of_le_range {G : Type u_1} [AddGroup G] {N : Type u_6} [AddGroup N] (H : AddSubgroup G) {f : N →+ G} (hf : Function.Injective f) (h : H.normalizer f.range) :
                                                                                                                                                              AddSubgroup.comap f H.normalizer = (AddSubgroup.comap f H).normalizer
                                                                                                                                                              theorem Subgroup.comap_normalizer_eq_of_injective_of_le_range {G : Type u_1} [Group G] {N : Type u_6} [Group N] (H : Subgroup G) {f : N →* G} (hf : Function.Injective f) (h : H.normalizer f.range) :
                                                                                                                                                              Subgroup.comap f H.normalizer = (Subgroup.comap f H).normalizer
                                                                                                                                                              theorem AddSubgroup.addSubgroupOf_normalizer_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : AddSubgroup G} (h : H.normalizer N) :
                                                                                                                                                              H.normalizer.addSubgroupOf N = (H.addSubgroupOf N).normalizer
                                                                                                                                                              theorem Subgroup.subgroupOf_normalizer_eq {G : Type u_1} [Group G] {H : Subgroup G} {N : Subgroup G} (h : H.normalizer N) :
                                                                                                                                                              H.normalizer.subgroupOf N = (H.subgroupOf N).normalizer
                                                                                                                                                              theorem AddSubgroup.map_equiv_normalizer_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G ≃+ N) :
                                                                                                                                                              AddSubgroup.map f.toAddMonoidHom H.normalizer = (AddSubgroup.map f.toAddMonoidHom H).normalizer

                                                                                                                                                              The image of the normalizer is equal to the normalizer of the image of an isomorphism.

                                                                                                                                                              theorem Subgroup.map_equiv_normalizer_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G ≃* N) :
                                                                                                                                                              Subgroup.map f.toMonoidHom H.normalizer = (Subgroup.map f.toMonoidHom H).normalizer

                                                                                                                                                              The image of the normalizer is equal to the normalizer of the image of an isomorphism.

                                                                                                                                                              theorem AddSubgroup.map_normalizer_eq_of_bijective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} (hf : Function.Bijective f) :
                                                                                                                                                              AddSubgroup.map f H.normalizer = (AddSubgroup.map f H).normalizer

                                                                                                                                                              The image of the normalizer is equal to the normalizer of the image of a bijective function.

                                                                                                                                                              theorem Subgroup.map_normalizer_eq_of_bijective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : G →* N} (hf : Function.Bijective f) :
                                                                                                                                                              Subgroup.map f H.normalizer = (Subgroup.map f H).normalizer

                                                                                                                                                              The image of the normalizer is equal to the normalizer of the image of a bijective function.

                                                                                                                                                              theorem AddMonoidHom.liftOfRightInverseAux.proof_2 {G₁ : Type u_3} {G₂ : Type u_2} {G₃ : Type u_1} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : G₁ →+ G₃) (hg : f.ker g.ker) (x : G₂) (y : G₂) :
                                                                                                                                                              { toFun := fun (b : G₂) => g (f_inv b), map_zero' := }.toFun (x + y) = { toFun := fun (b : G₂) => g (f_inv b), map_zero' := }.toFun x + { toFun := fun (b : G₂) => g (f_inv b), map_zero' := }.toFun y
                                                                                                                                                              theorem AddMonoidHom.liftOfRightInverseAux.proof_1 {G₁ : Type u_1} {G₂ : Type u_3} {G₃ : Type u_2} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : G₁ →+ G₃) (hg : f.ker g.ker) :
                                                                                                                                                              f_inv 0 g.ker
                                                                                                                                                              def AddMonoidHom.liftOfRightInverseAux {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : G₁ →+ G₃) (hg : f.ker g.ker) :
                                                                                                                                                              G₂ →+ G₃

                                                                                                                                                              Auxiliary definition used to define liftOfRightInverse

                                                                                                                                                              Equations
                                                                                                                                                              • f.liftOfRightInverseAux f_inv hf g hg = { toFun := fun (b : G₂) => g (f_inv b), map_zero' := , map_add' := }
                                                                                                                                                              Instances For
                                                                                                                                                                def MonoidHom.liftOfRightInverseAux {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃) (hg : f.ker g.ker) :
                                                                                                                                                                G₂ →* G₃

                                                                                                                                                                Auxiliary definition used to define liftOfRightInverse

                                                                                                                                                                Equations
                                                                                                                                                                • f.liftOfRightInverseAux f_inv hf g hg = { toFun := fun (b : G₂) => g (f_inv b), map_one' := , map_mul' := }
                                                                                                                                                                Instances For
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem AddMonoidHom.liftOfRightInverseAux_comp_apply {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : G₁ →+ G₃) (hg : f.ker g.ker) (x : G₁) :
                                                                                                                                                                  (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem MonoidHom.liftOfRightInverseAux_comp_apply {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃) (hg : f.ker g.ker) (x : G₁) :
                                                                                                                                                                  (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x
                                                                                                                                                                  def AddMonoidHom.liftOfRightInverse {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) :
                                                                                                                                                                  { g : G₁ →+ G₃ // f.ker g.ker } (G₂ →+ G₃)

                                                                                                                                                                  liftOfRightInverse f f_inv hf g hg is the unique additive group homomorphism φ

                                                                                                                                                                     G₁.
                                                                                                                                                                     |  \
                                                                                                                                                                   f |   \ g
                                                                                                                                                                     |    \
                                                                                                                                                                     v     \⌟
                                                                                                                                                                     G₂----> G₃
                                                                                                                                                                        ∃!φ
                                                                                                                                                                  
                                                                                                                                                                  Equations
                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                  Instances For
                                                                                                                                                                    theorem AddMonoidHom.liftOfRightInverse.proof_3 {G₁ : Type u_1} {G₂ : Type u_3} {G₃ : Type u_2} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : { g : G₁ →+ G₃ // f.ker g.ker }) :
                                                                                                                                                                    (fun (φ : G₂ →+ G₃) => φ.comp f, ) ((fun (g : { g : G₁ →+ G₃ // f.ker g.ker }) => f.liftOfRightInverseAux f_inv hf g ) g) = g
                                                                                                                                                                    theorem AddMonoidHom.liftOfRightInverse.proof_2 {G₁ : Type u_1} {G₂ : Type u_2} {G₃ : Type u_3} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (φ : G₂ →+ G₃) (x : G₁) (hx : x f.ker) :
                                                                                                                                                                    x (φ.comp f).ker
                                                                                                                                                                    theorem AddMonoidHom.liftOfRightInverse.proof_4 {G₁ : Type u_3} {G₂ : Type u_1} {G₃ : Type u_2} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (φ : G₂ →+ G₃) :
                                                                                                                                                                    (fun (g : { g : G₁ →+ G₃ // f.ker g.ker }) => f.liftOfRightInverseAux f_inv hf g ) ((fun (φ : G₂ →+ G₃) => φ.comp f, ) φ) = φ
                                                                                                                                                                    theorem AddMonoidHom.liftOfRightInverse.proof_1 {G₁ : Type u_1} {G₂ : Type u_2} {G₃ : Type u_3} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (g : { g : G₁ →+ G₃ // f.ker g.ker }) :
                                                                                                                                                                    f.ker (↑g).ker
                                                                                                                                                                    def MonoidHom.liftOfRightInverse {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) :
                                                                                                                                                                    { g : G₁ →* G₃ // f.ker g.ker } (G₂ →* G₃)

                                                                                                                                                                    liftOfRightInverse f hf g hg is the unique group homomorphism φ

                                                                                                                                                                    See MonoidHom.eq_liftOfRightInverse for the uniqueness lemma.

                                                                                                                                                                       G₁.
                                                                                                                                                                       |  \
                                                                                                                                                                     f |   \ g
                                                                                                                                                                       |    \
                                                                                                                                                                       v     \⌟
                                                                                                                                                                       G₂----> G₃
                                                                                                                                                                          ∃!φ
                                                                                                                                                                    
                                                                                                                                                                    Equations
                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[reducible, inline]
                                                                                                                                                                      noncomputable abbrev AddMonoidHom.liftOfSurjective {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (hf : Function.Surjective f) :
                                                                                                                                                                      { g : G₁ →+ G₃ // f.ker g.ker } (G₂ →+ G₃)

                                                                                                                                                                      A non-computable version of AddMonoidHom.liftOfRightInverse for when no computable right inverse is available.

                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        theorem AddMonoidHom.liftOfSurjective.proof_1 {G₁ : Type u_1} {G₂ : Type u_2} [AddGroup G₁] [AddGroup G₂] (f : G₁ →+ G₂) (hf : Function.Surjective f) :
                                                                                                                                                                        @[reducible, inline]
                                                                                                                                                                        noncomputable abbrev MonoidHom.liftOfSurjective {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (hf : Function.Surjective f) :
                                                                                                                                                                        { g : G₁ →* G₃ // f.ker g.ker } (G₂ →* G₃)

                                                                                                                                                                        A non-computable version of MonoidHom.liftOfRightInverse for when no computable right inverse is available, that uses Function.surjInv.

                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem AddMonoidHom.liftOfRightInverse_comp_apply {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : { g : G₁ →+ G₃ // f.ker g.ker }) (x : G₁) :
                                                                                                                                                                          ((f.liftOfRightInverse f_inv hf) g) (f x) = g x
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem MonoidHom.liftOfRightInverse_comp_apply {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : { g : G₁ →* G₃ // f.ker g.ker }) (x : G₁) :
                                                                                                                                                                          ((f.liftOfRightInverse f_inv hf) g) (f x) = g x
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem AddMonoidHom.liftOfRightInverse_comp {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : { g : G₁ →+ G₃ // f.ker g.ker }) :
                                                                                                                                                                          ((f.liftOfRightInverse f_inv hf) g).comp f = g
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem MonoidHom.liftOfRightInverse_comp {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : { g : G₁ →* G₃ // f.ker g.ker }) :
                                                                                                                                                                          ((f.liftOfRightInverse f_inv hf) g).comp f = g
                                                                                                                                                                          theorem AddMonoidHom.eq_liftOfRightInverse {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : G₁ →+ G₃) (hg : f.ker g.ker) (h : G₂ →+ G₃) (hh : h.comp f = g) :
                                                                                                                                                                          h = (f.liftOfRightInverse f_inv hf) g, hg
                                                                                                                                                                          theorem MonoidHom.eq_liftOfRightInverse {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂G₁) (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃) (hg : f.ker g.ker) (h : G₂ →* G₃) (hh : h.comp f = g) :
                                                                                                                                                                          h = (f.liftOfRightInverse f_inv hf) g, hg
                                                                                                                                                                          theorem AddSubgroup.Normal.comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup N} (hH : H.Normal) (f : G →+ N) :
                                                                                                                                                                          (AddSubgroup.comap f H).Normal
                                                                                                                                                                          theorem Subgroup.Normal.comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup N} (hH : H.Normal) (f : G →* N) :
                                                                                                                                                                          (Subgroup.comap f H).Normal
                                                                                                                                                                          @[instance 100]
                                                                                                                                                                          instance AddSubgroup.normal_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup N} [nH : H.Normal] (f : G →+ N) :
                                                                                                                                                                          (AddSubgroup.comap f H).Normal
                                                                                                                                                                          Equations
                                                                                                                                                                          • =
                                                                                                                                                                          @[instance 100]
                                                                                                                                                                          instance Subgroup.normal_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup N} [nH : H.Normal] (f : G →* N) :
                                                                                                                                                                          (Subgroup.comap f H).Normal
                                                                                                                                                                          Equations
                                                                                                                                                                          • =
                                                                                                                                                                          theorem AddSubgroup.Normal.addSubgroupOf {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : H.Normal) (K : AddSubgroup G) :
                                                                                                                                                                          (H.addSubgroupOf K).Normal
                                                                                                                                                                          theorem Subgroup.Normal.subgroupOf {G : Type u_1} [Group G] {H : Subgroup G} (hH : H.Normal) (K : Subgroup G) :
                                                                                                                                                                          (H.subgroupOf K).Normal
                                                                                                                                                                          @[instance 100]
                                                                                                                                                                          instance AddSubgroup.normal_addSubgroupOf {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : AddSubgroup G} [N.Normal] :
                                                                                                                                                                          (N.addSubgroupOf H).Normal
                                                                                                                                                                          Equations
                                                                                                                                                                          • =
                                                                                                                                                                          @[instance 100]
                                                                                                                                                                          instance Subgroup.normal_subgroupOf {G : Type u_1} [Group G] {H : Subgroup G} {N : Subgroup G} [N.Normal] :
                                                                                                                                                                          (N.subgroupOf H).Normal
                                                                                                                                                                          Equations
                                                                                                                                                                          • =
                                                                                                                                                                          theorem Subgroup.map_normalClosure {G : Type u_1} [Group G] {N : Type u_5} [Group N] (s : Set G) (f : G →* N) (hf : Function.Surjective f) :
                                                                                                                                                                          theorem Subgroup.comap_normalClosure {G : Type u_1} [Group G] {N : Type u_5} [Group N] (s : Set N) (f : G ≃* N) :
                                                                                                                                                                          theorem Subgroup.Normal.of_map_injective {G : Type u_6} {H : Type u_7} [Group G] [Group H] {φ : G →* H} (hφ : Function.Injective φ) {L : Subgroup G} (n : (Subgroup.map φ L).Normal) :
                                                                                                                                                                          L.Normal
                                                                                                                                                                          theorem Subgroup.Normal.of_map_subtype {G : Type u_1} [Group G] {K : Subgroup G} {L : Subgroup { x : G // x K }} (n : (Subgroup.map K.subtype L).Normal) :
                                                                                                                                                                          L.Normal
                                                                                                                                                                          def AddMonoidHom.addSubgroupComap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H' : AddSubgroup G') :
                                                                                                                                                                          { x : G // x AddSubgroup.comap f H' } →+ { x : G' // x H' }

                                                                                                                                                                          the AddMonoidHom from the preimage of an additive subgroup to itself.

                                                                                                                                                                          Equations
                                                                                                                                                                          • f.addSubgroupComap H' = f.addSubmonoidComap H'.toAddSubmonoid
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem AddMonoidHom.addSubgroupComap_apply_coe {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H' : AddSubgroup G') (x : { x : G // x AddSubmonoid.comap f H'.toAddSubmonoid }) :
                                                                                                                                                                            ((f.addSubgroupComap H') x) = f x
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem MonoidHom.subgroupComap_apply_coe {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H' : Subgroup G') (x : { x : G // x Submonoid.comap f H'.toSubmonoid }) :
                                                                                                                                                                            ((f.subgroupComap H') x) = f x
                                                                                                                                                                            def MonoidHom.subgroupComap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H' : Subgroup G') :
                                                                                                                                                                            { x : G // x Subgroup.comap f H' } →* { x : G' // x H' }

                                                                                                                                                                            The MonoidHom from the preimage of a subgroup to itself.

                                                                                                                                                                            Equations
                                                                                                                                                                            • f.subgroupComap H' = f.submonoidComap H'.toSubmonoid
                                                                                                                                                                            Instances For
                                                                                                                                                                              def AddMonoidHom.addSubgroupMap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) :
                                                                                                                                                                              { x : G // x H } →+ { x : G' // x AddSubgroup.map f H }

                                                                                                                                                                              the AddMonoidHom from an additive subgroup to its image

                                                                                                                                                                              Equations
                                                                                                                                                                              • f.addSubgroupMap H = f.addSubmonoidMap H.toAddSubmonoid
                                                                                                                                                                              Instances For
                                                                                                                                                                                @[simp]
                                                                                                                                                                                theorem AddMonoidHom.addSubgroupMap_apply_coe {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) (x : { x : G // x H.toAddSubmonoid }) :
                                                                                                                                                                                ((f.addSubgroupMap H) x) = f x
                                                                                                                                                                                @[simp]
                                                                                                                                                                                theorem MonoidHom.subgroupMap_apply_coe {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) (x : { x : G // x H.toSubmonoid }) :
                                                                                                                                                                                ((f.subgroupMap H) x) = f x
                                                                                                                                                                                def MonoidHom.subgroupMap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) :
                                                                                                                                                                                { x : G // x H } →* { x : G' // x Subgroup.map f H }

                                                                                                                                                                                The MonoidHom from a subgroup to its image.

                                                                                                                                                                                Equations
                                                                                                                                                                                • f.subgroupMap H = f.submonoidMap H.toSubmonoid
                                                                                                                                                                                Instances For
                                                                                                                                                                                  theorem AddMonoidHom.addSubgroupMap_surjective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) :
                                                                                                                                                                                  Function.Surjective (f.addSubgroupMap H)
                                                                                                                                                                                  theorem MonoidHom.subgroupMap_surjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) :
                                                                                                                                                                                  Function.Surjective (f.subgroupMap H)
                                                                                                                                                                                  theorem AddEquiv.addSubgroupCongr.proof_2 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H = K) :
                                                                                                                                                                                  ∀ (x x_1 : { x : G // x H }), (Equiv.setCongr ).toFun (x + x_1) = (Equiv.setCongr ).toFun (x + x_1)
                                                                                                                                                                                  def AddEquiv.addSubgroupCongr {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H = K) :
                                                                                                                                                                                  { x : G // x H } ≃+ { x : G // x K }

                                                                                                                                                                                  Makes the identity additive isomorphism from a proof two subgroups of an additive group are equal.

                                                                                                                                                                                  Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    theorem AddEquiv.addSubgroupCongr.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H = K) :
                                                                                                                                                                                    H = K
                                                                                                                                                                                    def MulEquiv.subgroupCongr {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H = K) :
                                                                                                                                                                                    { x : G // x H } ≃* { x : G // x K }

                                                                                                                                                                                    Makes the identity isomorphism from a proof two subgroups of a multiplicative group are equal.

                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[simp]
                                                                                                                                                                                      theorem AddEquiv.addSubgroupCongr_apply {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H = K) (x : { x : G // x H }) :
                                                                                                                                                                                      @[simp]
                                                                                                                                                                                      theorem MulEquiv.subgroupCongr_apply {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H = K) (x : { x : G // x H }) :
                                                                                                                                                                                      ((MulEquiv.subgroupCongr h) x) = x
                                                                                                                                                                                      @[simp]
                                                                                                                                                                                      theorem AddEquiv.addSubgroupCongr_symm_apply {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H = K) (x : { x : G // x K }) :
                                                                                                                                                                                      ((AddEquiv.addSubgroupCongr h).symm x) = x
                                                                                                                                                                                      @[simp]
                                                                                                                                                                                      theorem MulEquiv.subgroupCongr_symm_apply {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H = K) (x : { x : G // x K }) :
                                                                                                                                                                                      ((MulEquiv.subgroupCongr h).symm x) = x
                                                                                                                                                                                      def AddEquiv.addSubgroupMap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) :
                                                                                                                                                                                      { x : G // x H } ≃+ { x : G' // x AddSubgroup.map (↑e) H }

                                                                                                                                                                                      An additive subgroup is isomorphic to its image under an isomorphism. If you only have an injective map, use AddSubgroup.equiv_map_of_injective.

                                                                                                                                                                                      Equations
                                                                                                                                                                                      • e.addSubgroupMap H = e.addSubmonoidMap H.toAddSubmonoid
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        def MulEquiv.subgroupMap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) :
                                                                                                                                                                                        { x : G // x H } ≃* { x : G' // x Subgroup.map (↑e) H }

                                                                                                                                                                                        A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map, use Subgroup.equiv_map_of_injective.

                                                                                                                                                                                        Equations
                                                                                                                                                                                        • e.subgroupMap H = e.submonoidMap H.toSubmonoid
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem AddEquiv.coe_addSubgroupMap_apply {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) (g : { x : G // x H }) :
                                                                                                                                                                                          ((e.addSubgroupMap H) g) = e g
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem MulEquiv.coe_subgroupMap_apply {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) (g : { x : G // x H }) :
                                                                                                                                                                                          ((e.subgroupMap H) g) = e g
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem AddEquiv.addSubgroupMap_symm_apply {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) (g : { x : G' // x AddSubgroup.map (↑e) H }) :
                                                                                                                                                                                          (e.addSubgroupMap H).symm g = e.symm g,
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem MulEquiv.subgroupMap_symm_apply {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) (g : { x : G' // x Subgroup.map (↑e) H }) :
                                                                                                                                                                                          (e.subgroupMap H).symm g = e.symm g,
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem AddSubgroup.equivMapOfInjective_coe_addEquiv {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (e : G ≃+ G') :
                                                                                                                                                                                          H.equivMapOfInjective e = e.addSubgroupMap H
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem Subgroup.equivMapOfInjective_coe_mulEquiv {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (e : G ≃* G') :
                                                                                                                                                                                          H.equivMapOfInjective e = e.subgroupMap H
                                                                                                                                                                                          theorem AddSubgroup.mem_sup {C : Type u_6} [AddCommGroup C] {s : AddSubgroup C} {t : AddSubgroup C} {x : C} :
                                                                                                                                                                                          x s t ys, zt, y + z = x
                                                                                                                                                                                          theorem Subgroup.mem_sup {C : Type u_6} [CommGroup C] {s : Subgroup C} {t : Subgroup C} {x : C} :
                                                                                                                                                                                          x s t ys, zt, y * z = x
                                                                                                                                                                                          theorem AddSubgroup.mem_sup' {C : Type u_6} [AddCommGroup C] {s : AddSubgroup C} {t : AddSubgroup C} {x : C} :
                                                                                                                                                                                          x s t ∃ (y : { x : C // x s }) (z : { x : C // x t }), y + z = x
                                                                                                                                                                                          theorem Subgroup.mem_sup' {C : Type u_6} [CommGroup C] {s : Subgroup C} {t : Subgroup C} {x : C} :
                                                                                                                                                                                          x s t ∃ (y : { x : C // x s }) (z : { x : C // x t }), y * z = x
                                                                                                                                                                                          theorem AddSubgroup.mem_closure_pair {C : Type u_6} [AddCommGroup C] {x : C} {y : C} {z : C} :
                                                                                                                                                                                          z AddSubgroup.closure {x, y} ∃ (m : ) (n : ), m x + n y = z
                                                                                                                                                                                          theorem Subgroup.mem_closure_pair {C : Type u_6} [CommGroup C] {x : C} {y : C} {z : C} :
                                                                                                                                                                                          z Subgroup.closure {x, y} ∃ (m : ) (n : ), x ^ m * y ^ n = z
                                                                                                                                                                                          theorem AddSubgroup.normal_addSubgroupOf_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (hHK : H K) :
                                                                                                                                                                                          (H.addSubgroupOf K).Normal ∀ (h k : G), h Hk Kk + h + -k H
                                                                                                                                                                                          theorem Subgroup.normal_subgroupOf_iff {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hHK : H K) :
                                                                                                                                                                                          (H.subgroupOf K).Normal ∀ (h k : G), h Hk Kk * h * k⁻¹ H
                                                                                                                                                                                          instance AddSubgroup.sum_addSubgroupOf_sum_normal {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H₁ : AddSubgroup G} {K₁ : AddSubgroup G} {H₂ : AddSubgroup N} {K₂ : AddSubgroup N} [h₁ : (H₁.addSubgroupOf K₁).Normal] [h₂ : (H₂.addSubgroupOf K₂).Normal] :
                                                                                                                                                                                          ((H₁.prod H₂).addSubgroupOf (K₁.prod K₂)).Normal
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • =
                                                                                                                                                                                          instance Subgroup.prod_subgroupOf_prod_normal {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H₁ : Subgroup G} {K₁ : Subgroup G} {H₂ : Subgroup N} {K₂ : Subgroup N} [h₁ : (H₁.subgroupOf K₁).Normal] [h₂ : (H₂.subgroupOf K₂).Normal] :
                                                                                                                                                                                          ((H₁.prod H₂).subgroupOf (K₁.prod K₂)).Normal
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • =
                                                                                                                                                                                          instance AddSubgroup.sum_normal {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) [hH : H.Normal] [hK : K.Normal] :
                                                                                                                                                                                          (H.prod K).Normal
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • =
                                                                                                                                                                                          instance Subgroup.prod_normal {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup N) [hH : H.Normal] [hK : K.Normal] :
                                                                                                                                                                                          (H.prod K).Normal
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • =
                                                                                                                                                                                          theorem AddSubgroup.inf_addSubgroupOf_inf_normal_of_right {G : Type u_1} [AddGroup G] (A : AddSubgroup G) (B' : AddSubgroup G) (B : AddSubgroup G) (hB : B' B) [hN : (B'.addSubgroupOf B).Normal] :
                                                                                                                                                                                          ((A B').addSubgroupOf (A B)).Normal
                                                                                                                                                                                          theorem Subgroup.inf_subgroupOf_inf_normal_of_right {G : Type u_1} [Group G] (A : Subgroup G) (B' : Subgroup G) (B : Subgroup G) (hB : B' B) [hN : (B'.subgroupOf B).Normal] :
                                                                                                                                                                                          ((A B').subgroupOf (A B)).Normal
                                                                                                                                                                                          theorem AddSubgroup.inf_addSubgroupOf_inf_normal_of_left {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} (B : AddSubgroup G) (hA : A' A) [hN : (A'.addSubgroupOf A).Normal] :
                                                                                                                                                                                          ((A' B).addSubgroupOf (A B)).Normal
                                                                                                                                                                                          theorem Subgroup.inf_subgroupOf_inf_normal_of_left {G : Type u_1} [Group G] {A' : Subgroup G} {A : Subgroup G} (B : Subgroup G) (hA : A' A) [hN : (A'.subgroupOf A).Normal] :
                                                                                                                                                                                          ((A' B).subgroupOf (A B)).Normal
                                                                                                                                                                                          instance AddSubgroup.normal_inf_normal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) [hH : H.Normal] [hK : K.Normal] :
                                                                                                                                                                                          (H K).Normal
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • =
                                                                                                                                                                                          instance Subgroup.normal_inf_normal {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) [hH : H.Normal] [hK : K.Normal] :
                                                                                                                                                                                          (H K).Normal
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • =
                                                                                                                                                                                          theorem AddSubgroup.addSubgroupOf_sup {G : Type u_1} [AddGroup G] (A : AddSubgroup G) (A' : AddSubgroup G) (B : AddSubgroup G) (hA : A B) (hA' : A' B) :
                                                                                                                                                                                          (A A').addSubgroupOf B = A.addSubgroupOf B A'.addSubgroupOf B
                                                                                                                                                                                          theorem Subgroup.subgroupOf_sup {G : Type u_1} [Group G] (A : Subgroup G) (A' : Subgroup G) (B : Subgroup G) (hA : A B) (hA' : A' B) :
                                                                                                                                                                                          (A A').subgroupOf B = A.subgroupOf B A'.subgroupOf B
                                                                                                                                                                                          theorem AddSubgroup.SubgroupNormal.mem_comm {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (hK : H K) [hN : (H.addSubgroupOf K).Normal] {a : G} {b : G} (hb : b K) (h : a + b H) :
                                                                                                                                                                                          b + a H
                                                                                                                                                                                          theorem Subgroup.SubgroupNormal.mem_comm {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hK : H K) [hN : (H.subgroupOf K).Normal] {a : G} {b : G} (hb : b K) (h : a * b H) :
                                                                                                                                                                                          b * a H
                                                                                                                                                                                          theorem AddSubgroup.addCommute_of_normal_of_disjoint {G : Type u_1} [AddGroup G] (H₁ : AddSubgroup G) (H₂ : AddSubgroup G) (hH₁ : H₁.Normal) (hH₂ : H₂.Normal) (hdis : Disjoint H₁ H₂) (x : G) (y : G) (hx : x H₁) (hy : y H₂) :

                                                                                                                                                                                          Elements of disjoint, normal subgroups commute.

                                                                                                                                                                                          theorem Subgroup.commute_of_normal_of_disjoint {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) (hH₁ : H₁.Normal) (hH₂ : H₂.Normal) (hdis : Disjoint H₁ H₂) (x : G) (y : G) (hx : x H₁) (hy : y H₂) :

                                                                                                                                                                                          Elements of disjoint, normal subgroups commute.

                                                                                                                                                                                          theorem AddSubgroup.disjoint_def {G : Type u_1} [AddGroup G] {H₁ : AddSubgroup G} {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₁ : Subgroup G} {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₁ : AddSubgroup G} {H₂ : AddSubgroup G} :
                                                                                                                                                                                          Disjoint H₁ H₂ ∀ {x y : G}, x H₁y H₂x = yx = 0
                                                                                                                                                                                          theorem Subgroup.disjoint_def' {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} :
                                                                                                                                                                                          Disjoint H₁ H₂ ∀ {x y : G}, x H₁y H₂x = yx = 1
                                                                                                                                                                                          theorem AddSubgroup.disjoint_iff_add_eq_zero {G : Type u_1} [AddGroup G] {H₁ : AddSubgroup G} {H₂ : AddSubgroup G} :
                                                                                                                                                                                          Disjoint H₁ H₂ ∀ {x y : G}, x H₁y H₂x + y = 0x = 0 y = 0
                                                                                                                                                                                          theorem Subgroup.disjoint_iff_mul_eq_one {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} :
                                                                                                                                                                                          Disjoint H₁ H₂ ∀ {x y : G}, x H₁y H₂x * y = 1x = 1 y = 1
                                                                                                                                                                                          theorem AddSubgroup.add_injective_of_disjoint {G : Type u_1} [AddGroup G] {H₁ : AddSubgroup G} {H₂ : AddSubgroup G} (h : Disjoint H₁ H₂) :
                                                                                                                                                                                          Function.Injective fun (g : { x : G // x H₁ } × { x : G // x H₂ }) => g.1 + g.2
                                                                                                                                                                                          theorem Subgroup.mul_injective_of_disjoint {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} (h : Disjoint H₁ H₂) :
                                                                                                                                                                                          Function.Injective fun (g : { x : G // x H₁ } × { x : G // x H₂ }) => g.1 * g.2
                                                                                                                                                                                          theorem IsConj.normalClosure_eq_top_of {G : Type u_1} [Group G] {N : Subgroup G} [hn : N.Normal] {g : G} {g' : G} {hg : g N} {hg' : g' N} (hc : IsConj g g') (ht : Subgroup.normalClosure {g, hg} = ) :
                                                                                                                                                                                          Subgroup.normalClosure {g', hg'} =

                                                                                                                                                                                          The conjugacy classes that are not trivial.

                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem ConjClasses.mem_noncenter {G : Type u_6} [Monoid G] (g : ConjClasses G) :
                                                                                                                                                                                            g ConjClasses.noncenter G g.carrier.Nontrivial