Documentation

Mathlib.GroupTheory.QuotientGroup.Basic

Quotients of groups by normal subgroups #

This files develops the basic theory of quotients of groups by normal subgroups. In particular it proves Noether's first and second isomorphism theorems.

Main definitions #

Main statements #

Tags #

isomorphism theorems, quotient groups

theorem QuotientAddGroup.con.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {a : G} {b : G} {c : G} {d : G} (hab : Setoid.r a b) (hcd : Setoid.r c d) :
Setoid.r (a + c) (b + d)
def QuotientAddGroup.con {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :

The additive congruence relation generated by a normal additive subgroup.

Equations
Instances For
    def QuotientGroup.con {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
    Con G

    The congruence relation generated by a normal subgroup.

    Equations
    Instances For
      instance QuotientGroup.Quotient.group {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
      Group (G N)
      Equations
      theorem QuotientAddGroup.mk'.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) :
      ∀ (x x_1 : G), (x + x_1) = (x + x_1)
      def QuotientAddGroup.mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :
      G →+ G N

      The additive group homomorphism from G to G/N.

      Equations
      Instances For
        def QuotientGroup.mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
        G →* G N

        The group homomorphism from G to G/N.

        Equations
        Instances For
          @[simp]
          theorem QuotientAddGroup.coe_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :
          (QuotientAddGroup.mk' N) = QuotientAddGroup.mk
          @[simp]
          theorem QuotientGroup.coe_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
          (QuotientGroup.mk' N) = QuotientGroup.mk
          @[simp]
          theorem QuotientAddGroup.mk'_apply {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (x : G) :
          @[simp]
          theorem QuotientGroup.mk'_apply {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (x : G) :
          (QuotientGroup.mk' N) x = x
          theorem QuotientAddGroup.mk'_eq_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {x : G} {y : G} :
          (QuotientAddGroup.mk' N) x = (QuotientAddGroup.mk' N) y zN, x + z = y
          theorem QuotientGroup.mk'_eq_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {x : G} {y : G} :
          (QuotientGroup.mk' N) x = (QuotientGroup.mk' N) y zN, x * z = y
          theorem QuotientAddGroup.sound {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (U : Set (G N)) (g : N.op) :
          theorem QuotientGroup.sound {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (U : Set (G N)) (g : N.op) :
          theorem QuotientAddGroup.addMonoidHom_ext {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] ⦃f : G N →+ M ⦃g : G N →+ M (h : f.comp (QuotientAddGroup.mk' N) = g.comp (QuotientAddGroup.mk' N)) :
          f = g

          Two AddMonoidHoms from an additive quotient group are equal if their compositions with AddQuotientGroup.mk' are equal.

          See note [partially-applied ext lemmas].

          theorem QuotientGroup.monoidHom_ext_iff {G : Type u} [Group G] {N : Subgroup G} [nN : N.Normal] {M : Type x} [Monoid M] {f : G N →* M} {g : G N →* M} :
          f = g f.comp (QuotientGroup.mk' N) = g.comp (QuotientGroup.mk' N)
          theorem QuotientAddGroup.addMonoidHom_ext_iff {G : Type u} [AddGroup G] {N : AddSubgroup G} [nN : N.Normal] {M : Type x} [AddMonoid M] {f : G N →+ M} {g : G N →+ M} :
          f = g f.comp (QuotientAddGroup.mk' N) = g.comp (QuotientAddGroup.mk' N)
          theorem QuotientGroup.monoidHom_ext {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] ⦃f : G N →* M ⦃g : G N →* M (h : f.comp (QuotientGroup.mk' N) = g.comp (QuotientGroup.mk' N)) :
          f = g

          Two MonoidHoms from a quotient group are equal if their compositions with QuotientGroup.mk' are equal.

          See note [partially-applied ext lemmas].

          @[simp]
          theorem QuotientAddGroup.eq_zero_iff {G : Type u} [AddGroup G] {N : AddSubgroup G} [nN : N.Normal] (x : G) :
          x = 0 x N
          @[simp]
          theorem QuotientGroup.eq_one_iff {G : Type u} [Group G] {N : Subgroup G} [nN : N.Normal] (x : G) :
          x = 1 x N
          theorem QuotientAddGroup.ker_le_range_iff {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] {I : Type w} [AddGroup I] (f : G →+ H) [f.range.Normal] (g : H →+ I) :
          g.ker f.range (QuotientAddGroup.mk' f.range).comp g.ker.subtype = 0
          theorem QuotientGroup.ker_le_range_iff {G : Type u} [Group G] {H : Type v} [Group H] {I : Type w} [Group I] (f : G →* H) [f.range.Normal] (g : H →* I) :
          g.ker f.range (QuotientGroup.mk' f.range).comp g.ker.subtype = 1
          @[simp]
          theorem QuotientAddGroup.ker_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :
          @[simp]
          theorem QuotientGroup.ker_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
          theorem QuotientAddGroup.eq_iff_sub_mem {G : Type u} [AddGroup G] {N : AddSubgroup G} [nN : N.Normal] {x : G} {y : G} :
          x = y x - y N
          theorem QuotientGroup.eq_iff_div_mem {G : Type u} [Group G] {N : Subgroup G} [nN : N.Normal] {x : G} {y : G} :
          x = y x / y N
          theorem QuotientAddGroup.Quotient.addCommGroup.proof_1 {G : Type u_1} [AddCommGroup G] (N : AddSubgroup G) (a : G N) (b : G N) :
          a + b = b + a
          @[simp]
          theorem QuotientAddGroup.mk_zero {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :
          0 = 0
          @[simp]
          theorem QuotientGroup.mk_one {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
          1 = 1
          @[simp]
          theorem QuotientAddGroup.mk_add {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (b : G) :
          (a + b) = a + b
          @[simp]
          theorem QuotientGroup.mk_mul {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (b : G) :
          (a * b) = a * b
          @[simp]
          theorem QuotientAddGroup.mk_neg {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) :
          (-a) = -a
          @[simp]
          theorem QuotientGroup.mk_inv {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) :
          a⁻¹ = (↑a)⁻¹
          @[simp]
          theorem QuotientAddGroup.mk_sub {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (b : G) :
          (a - b) = a - b
          @[simp]
          theorem QuotientGroup.mk_div {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (b : G) :
          (a / b) = a / b
          @[simp]
          theorem QuotientAddGroup.mk_nsmul {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (n : ) :
          (n a) = n a
          @[simp]
          theorem QuotientGroup.mk_pow {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (n : ) :
          (a ^ n) = a ^ n
          @[simp]
          theorem QuotientAddGroup.mk_zsmul {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (n : ) :
          (n a) = n a
          @[simp]
          theorem QuotientGroup.mk_zpow {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (n : ) :
          (a ^ n) = a ^ n
          @[simp]
          theorem QuotientAddGroup.mk_sum {G : Type u_1} {ι : Type u_2} [AddCommGroup G] (N : AddSubgroup G) (s : Finset ι) {f : ιG} :
          (s.sum f) = is, (f i)
          @[simp]
          theorem QuotientGroup.mk_prod {G : Type u_1} {ι : Type u_2} [CommGroup G] (N : Subgroup G) (s : Finset ι) {f : ιG} :
          (s.prod f) = is, (f i)
          @[simp]
          @[simp]
          theorem QuotientGroup.map_mk'_self {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
          def QuotientAddGroup.lift {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] (φ : G →+ M) (HN : N φ.ker) :
          G N →+ M

          An AddGroup homomorphism φ : G →+ M with N ⊆ ker(φ) descends (i.e. lifts) to a group homomorphism G/N →* M.

          Equations
          Instances For
            theorem QuotientAddGroup.lift.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type u_2} [AddMonoid M] (φ : G →+ M) (HN : N φ.ker) (x : G) (y : G) (h : (QuotientAddGroup.con N) x y) :
            (AddCon.ker φ) x y
            def QuotientGroup.lift {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] (φ : G →* M) (HN : N φ.ker) :
            G N →* M

            A group homomorphism φ : G →* M with N ⊆ ker(φ) descends (i.e. lifts) to a group homomorphism G/N →* M.

            Equations
            Instances For
              @[simp]
              theorem QuotientAddGroup.lift_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N φ.ker) (g : G) :
              (QuotientAddGroup.lift N φ HN) g = φ g
              @[simp]
              theorem QuotientGroup.lift_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] {φ : G →* M} (HN : N φ.ker) (g : G) :
              (QuotientGroup.lift N φ HN) g = φ g
              @[simp]
              theorem QuotientAddGroup.lift_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N φ.ker) (g : G) :
              (QuotientAddGroup.lift N φ HN) g = φ g
              @[simp]
              theorem QuotientGroup.lift_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] {φ : G →* M} (HN : N φ.ker) (g : G) :
              (QuotientGroup.lift N φ HN) g = φ g
              @[simp]
              theorem QuotientAddGroup.lift_quot_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N φ.ker) (g : G) :
              (QuotientAddGroup.lift N φ HN) (Quot.mk Setoid.r g) = φ g
              @[simp]
              theorem QuotientGroup.lift_quot_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] {φ : G →* M} (HN : N φ.ker) (g : G) :
              (QuotientGroup.lift N φ HN) (Quot.mk Setoid.r g) = φ g
              theorem QuotientAddGroup.map.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) {H : Type u_2} [AddGroup H] (M : AddSubgroup H) (f : G →+ H) (h : N AddSubgroup.comap f M) ⦃x : G (hx : x N) :
              (f x) = 0
              def QuotientAddGroup.map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N AddSubgroup.comap f M) :
              G N →+ H M

              An AddGroup homomorphism f : G →+ H induces a map G/N →+ H/M if N ⊆ f⁻¹(M).

              Equations
              Instances For
                def QuotientGroup.map {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N Subgroup.comap f M) :
                G N →* H M

                A group homomorphism f : G →* H induces a map G/N →* H/M if N ⊆ f⁻¹(M).

                Equations
                Instances For
                  @[simp]
                  theorem QuotientAddGroup.map_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N AddSubgroup.comap f M) (x : G) :
                  (QuotientAddGroup.map N M f h) x = (f x)
                  @[simp]
                  theorem QuotientGroup.map_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N Subgroup.comap f M) (x : G) :
                  (QuotientGroup.map N M f h) x = (f x)
                  theorem QuotientAddGroup.map_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N AddSubgroup.comap f M) (x : G) :
                  (QuotientAddGroup.map N M f h) ((QuotientAddGroup.mk' N) x) = (f x)
                  theorem QuotientGroup.map_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N Subgroup.comap f M) (x : G) :
                  (QuotientGroup.map N M f h) ((QuotientGroup.mk' N) x) = (f x)
                  theorem QuotientAddGroup.map_id_apply {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (h : optParam (N AddSubgroup.comap (AddMonoidHom.id G) N) ) (x : G N) :
                  theorem QuotientGroup.map_id_apply {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (h : optParam (N Subgroup.comap (MonoidHom.id G) N) ) (x : G N) :
                  @[simp]
                  @[simp]
                  theorem QuotientGroup.map_id {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (h : optParam (N Subgroup.comap (MonoidHom.id G) N) ) :
                  @[simp]
                  theorem QuotientAddGroup.map_map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] {I : Type u_1} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [M.Normal] [O.Normal] (f : G →+ H) (g : H →+ I) (hf : N AddSubgroup.comap f M) (hg : M AddSubgroup.comap g O) (hgf : optParam (N AddSubgroup.comap (g.comp f) O) ) (x : G N) :
                  (QuotientAddGroup.map M O g hg) ((QuotientAddGroup.map N M f hf) x) = (QuotientAddGroup.map N O (g.comp f) hgf) x
                  @[simp]
                  theorem QuotientGroup.map_map {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] {I : Type u_1} [Group I] (M : Subgroup H) (O : Subgroup I) [M.Normal] [O.Normal] (f : G →* H) (g : H →* I) (hf : N Subgroup.comap f M) (hg : M Subgroup.comap g O) (hgf : optParam (N Subgroup.comap (g.comp f) O) ) (x : G N) :
                  (QuotientGroup.map M O g hg) ((QuotientGroup.map N M f hf) x) = (QuotientGroup.map N O (g.comp f) hgf) x
                  @[simp]
                  theorem QuotientAddGroup.map_comp_map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] {I : Type u_1} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [M.Normal] [O.Normal] (f : G →+ H) (g : H →+ I) (hf : N AddSubgroup.comap f M) (hg : M AddSubgroup.comap g O) (hgf : optParam (N AddSubgroup.comap (g.comp f) O) ) :
                  (QuotientAddGroup.map M O g hg).comp (QuotientAddGroup.map N M f hf) = QuotientAddGroup.map N O (g.comp f) hgf
                  @[simp]
                  theorem QuotientGroup.map_comp_map {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] {I : Type u_1} [Group I] (M : Subgroup H) (O : Subgroup I) [M.Normal] [O.Normal] (f : G →* H) (g : H →* I) (hf : N Subgroup.comap f M) (hg : M Subgroup.comap g O) (hgf : optParam (N Subgroup.comap (g.comp f) O) ) :
                  (QuotientGroup.map M O g hg).comp (QuotientGroup.map N M f hf) = QuotientGroup.map N O (g.comp f) hgf
                  @[simp]
                  theorem QuotientAddGroup.image_coe {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :
                  QuotientAddGroup.mk '' N = 0
                  @[simp]
                  theorem QuotientGroup.image_coe {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
                  QuotientGroup.mk '' N = 1
                  theorem QuotientAddGroup.preimage_image_coe {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (s : Set G) :
                  QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = N + s
                  theorem QuotientGroup.preimage_image_coe {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (s : Set G) :
                  QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = N * s
                  theorem QuotientAddGroup.image_coe_inj {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {s : Set G} {t : Set G} :
                  QuotientAddGroup.mk '' s = QuotientAddGroup.mk '' t N + s = N + t
                  theorem QuotientGroup.image_coe_inj {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {s : Set G} {t : Set G} :
                  QuotientGroup.mk '' s = QuotientGroup.mk '' t N * s = N * t
                  theorem QuotientAddGroup.congr.proof_5 {G : Type u_2} [AddGroup G] {H : Type u_1} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') :
                  H' AddSubgroup.comap (↑e.symm) G'
                  theorem QuotientAddGroup.congr.proof_6 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') (x : G G') :
                  (QuotientAddGroup.map H' G' e.symm ) ((QuotientAddGroup.map G' H' e ) x) = x
                  theorem QuotientAddGroup.congr.proof_3 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') :
                  G' AddSubgroup.comap (↑e) H'
                  theorem QuotientAddGroup.congr.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') :
                  G' AddSubgroup.comap (↑e) H'
                  theorem QuotientAddGroup.congr.proof_7 {G : Type u_2} [AddGroup G] {H : Type u_1} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') (x : H H') :
                  (QuotientAddGroup.map G' H' e ) ((QuotientAddGroup.map H' G' e.symm ) x) = x
                  theorem QuotientAddGroup.congr.proof_8 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') (x : G G') (y : G G') :
                  (↑(QuotientAddGroup.map G' H' e )).toFun (x + y) = (↑(QuotientAddGroup.map G' H' e )).toFun x + (↑(QuotientAddGroup.map G' H' e )).toFun y
                  def QuotientAddGroup.congr {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') :
                  G G' ≃+ H H'

                  QuotientAddGroup.congr lifts the isomorphism e : G ≃ H to G ⧸ G' ≃ H ⧸ H', given that e maps G to H.

                  Equations
                  Instances For
                    def QuotientGroup.congr {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') :
                    G G' ≃* H H'

                    QuotientGroup.congr lifts the isomorphism e : G ≃ H to G ⧸ G' ≃ H ⧸ H', given that e maps G to H.

                    Equations
                    Instances For
                      @[simp]
                      theorem QuotientGroup.congr_mk {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) :
                      (QuotientGroup.congr G' H' e he) x = (e x)
                      theorem QuotientGroup.congr_mk' {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) :
                      (QuotientGroup.congr G' H' e he) ((QuotientGroup.mk' G') x) = (QuotientGroup.mk' H') (e x)
                      @[simp]
                      theorem QuotientGroup.congr_apply {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) :
                      (QuotientGroup.congr G' H' e he) x = (QuotientGroup.mk' H') (e x)
                      @[simp]
                      theorem QuotientGroup.congr_refl {G : Type u} [Group G] (G' : Subgroup G) [G'.Normal] (he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') ) :
                      @[simp]
                      theorem QuotientGroup.congr_symm {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') :
                      (QuotientGroup.congr G' H' e he).symm = QuotientGroup.congr H' G' e.symm
                      def QuotientAddGroup.kerLift {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) :
                      G φ.ker →+ H

                      The induced map from the quotient by the kernel to the codomain.

                      Equations
                      Instances For
                        theorem QuotientAddGroup.kerLift.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (_g : G) :
                        _g φ.kerφ _g = 0
                        theorem QuotientAddGroup.kerLift.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) :
                        φ.ker.Normal
                        def QuotientGroup.kerLift {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
                        G φ.ker →* H

                        The induced map from the quotient by the kernel to the codomain.

                        Equations
                        Instances For
                          @[simp]
                          theorem QuotientAddGroup.kerLift_mk {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (g : G) :
                          @[simp]
                          theorem QuotientGroup.kerLift_mk {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (g : G) :
                          (QuotientGroup.kerLift φ) g = φ g
                          @[simp]
                          theorem QuotientAddGroup.kerLift_mk' {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (g : G) :
                          @[simp]
                          theorem QuotientGroup.kerLift_mk' {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (g : G) :
                          (QuotientGroup.kerLift φ) g = φ g
                          theorem QuotientAddGroup.rangeKerLift.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (g : G) (hg : g φ.ker) :
                          φ.rangeRestrict g = 0
                          theorem QuotientAddGroup.rangeKerLift.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) :
                          φ.ker.Normal
                          def QuotientAddGroup.rangeKerLift {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) :
                          G φ.ker →+ φ.range

                          The induced map from the quotient by the kernel to the range.

                          Equations
                          Instances For
                            def QuotientGroup.rangeKerLift {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
                            G φ.ker →* φ.range

                            The induced map from the quotient by the kernel to the range.

                            Equations
                            Instances For
                              theorem QuotientAddGroup.quotientKerEquivRange.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) :
                              φ.ker.Normal
                              theorem QuotientAddGroup.quotientKerEquivRange.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) :
                              AddHomClass (G φ.ker →+ φ.range) (G φ.ker) φ.range
                              noncomputable def QuotientAddGroup.quotientKerEquivRange {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) :
                              G φ.ker ≃+ φ.range

                              The first isomorphism theorem (a definition): the canonical isomorphism between G/(ker φ) to range φ.

                              Equations
                              Instances For
                                noncomputable def QuotientGroup.quotientKerEquivRange {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
                                G φ.ker ≃* φ.range

                                Noether's first isomorphism theorem (a definition): the canonical isomorphism between G/(ker φ) to range φ.

                                Equations
                                Instances For
                                  def QuotientAddGroup.quotientKerEquivOfRightInverse {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : HG) (hφ : Function.RightInverse ψ φ) :
                                  G φ.ker ≃+ H

                                  The canonical isomorphism G/(ker φ) ≃+ H induced by a homomorphism φ : G →+ H with a right inverse ψ : H → G.

                                  Equations
                                  Instances For
                                    theorem QuotientAddGroup.quotientKerEquivOfRightInverse.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (ψ : HG) (hφ : Function.RightInverse ψ φ) (x : G φ.ker) :
                                    (QuotientAddGroup.mk ψ) ((QuotientAddGroup.kerLift φ) x) = x
                                    theorem QuotientAddGroup.quotientKerEquivOfRightInverse.proof_3 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (x : G φ.ker) (y : G φ.ker) :
                                    (↑(QuotientAddGroup.kerLift φ)).toFun (x + y) = (↑(QuotientAddGroup.kerLift φ)).toFun x + (↑(QuotientAddGroup.kerLift φ)).toFun y
                                    theorem QuotientAddGroup.quotientKerEquivOfRightInverse.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) :
                                    φ.ker.Normal
                                    @[simp]
                                    theorem QuotientGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : HG) (hφ : Function.RightInverse ψ φ) (a : G φ.ker) :
                                    @[simp]
                                    theorem QuotientAddGroup.quotientKerEquivOfRightInverse_symm_apply {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : HG) (hφ : Function.RightInverse ψ φ) :
                                    ∀ (a : H), (QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ ).symm a = (QuotientAddGroup.mk ψ) a
                                    @[simp]
                                    theorem QuotientAddGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : HG) (hφ : Function.RightInverse ψ φ) (a : G φ.ker) :
                                    @[simp]
                                    theorem QuotientGroup.quotientKerEquivOfRightInverse_symm_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : HG) (hφ : Function.RightInverse ψ φ) :
                                    ∀ (a : H), (QuotientGroup.quotientKerEquivOfRightInverse φ ψ ).symm a = (QuotientGroup.mk ψ) a
                                    def QuotientGroup.quotientKerEquivOfRightInverse {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : HG) (hφ : Function.RightInverse ψ φ) :
                                    G φ.ker ≃* H

                                    The canonical isomorphism G/(ker φ) ≃* H induced by a homomorphism φ : G →* H with a right inverse ψ : H → G.

                                    Equations
                                    Instances For

                                      The canonical isomorphism G/⊥ ≃+ G.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem QuotientGroup.quotientBot_symm_apply {G : Type u} [Group G] :
                                        ∀ (a : G), QuotientGroup.quotientBot.symm a = a
                                        @[simp]
                                        theorem QuotientAddGroup.quotientBot_symm_apply {G : Type u} [AddGroup G] :
                                        ∀ (a : G), QuotientAddGroup.quotientBot.symm a = a
                                        @[simp]
                                        theorem QuotientAddGroup.quotientBot_apply {G : Type u} [AddGroup G] (a : G (AddMonoidHom.id G).ker) :
                                        QuotientAddGroup.quotientBot a = (QuotientAddGroup.kerLift (AddMonoidHom.id G)) a
                                        @[simp]
                                        theorem QuotientGroup.quotientBot_apply {G : Type u} [Group G] (a : G (MonoidHom.id G).ker) :
                                        QuotientGroup.quotientBot a = (QuotientGroup.kerLift (MonoidHom.id G)) a

                                        The canonical isomorphism G/⊥ ≃* G.

                                        Equations
                                        Instances For
                                          noncomputable def QuotientAddGroup.quotientKerEquivOfSurjective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (hφ : Function.Surjective φ) :
                                          G φ.ker ≃+ H

                                          The canonical isomorphism G/(ker φ) ≃+ H induced by a surjection φ : G →+ H. For a computable version, see QuotientAddGroup.quotientKerEquivOfRightInverse.

                                          Equations
                                          Instances For
                                            noncomputable def QuotientGroup.quotientKerEquivOfSurjective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (hφ : Function.Surjective φ) :
                                            G φ.ker ≃* H

                                            The canonical isomorphism G/(ker φ) ≃* H induced by a surjection φ : G →* H.

                                            For a computable version, see QuotientGroup.quotientKerEquivOfRightInverse.

                                            Equations
                                            Instances For
                                              def QuotientAddGroup.quotientAddEquivOfEq {G : Type u} [AddGroup G] {M : AddSubgroup G} {N : AddSubgroup G} [M.Normal] [N.Normal] (h : M = N) :
                                              G M ≃+ G N

                                              If two normal subgroups M and N of G are the same, their quotient groups are isomorphic.

                                              Equations
                                              Instances For
                                                theorem QuotientAddGroup.quotientAddEquivOfEq.proof_1 {G : Type u_1} [AddGroup G] {M : AddSubgroup G} {N : AddSubgroup G} [M.Normal] [N.Normal] (h : M = N) (q : G M) (r : G M) :
                                                def QuotientGroup.quotientMulEquivOfEq {G : Type u} [Group G] {M : Subgroup G} {N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) :
                                                G M ≃* G N

                                                If two normal subgroups M and N of G are the same, their quotient groups are isomorphic.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem QuotientAddGroup.quotientAddEquivOfEq_mk {G : Type u} [AddGroup G] {M : AddSubgroup G} {N : AddSubgroup G} [M.Normal] [N.Normal] (h : M = N) (x : G) :
                                                  @[simp]
                                                  theorem QuotientGroup.quotientMulEquivOfEq_mk {G : Type u} [Group G] {M : Subgroup G} {N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) (x : G) :
                                                  def QuotientAddGroup.quotientMapAddSubgroupOfOfLe {G : Type u} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} {B : AddSubgroup G} [_hAN : (A'.addSubgroupOf A).Normal] [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' B') (h : A B) :
                                                  A A'.addSubgroupOf A →+ B B'.addSubgroupOf B

                                                  Let A', A, B', B be subgroups of G. If A' ≤ B' and A ≤ B, then there is a map A / (A' ⊓ A) →+ B / (B' ⊓ B) induced by the inclusions.

                                                  Equations
                                                  Instances For
                                                    theorem QuotientAddGroup.quotientMapAddSubgroupOfOfLe.proof_1 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} (h' : A' B') :
                                                    AddSubgroup.comap A.subtype A' AddSubgroup.comap A.subtype B'
                                                    def QuotientGroup.quotientMapSubgroupOfOfLe {G : Type u} [Group G] {A' : Subgroup G} {A : Subgroup G} {B' : Subgroup G} {B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal] [_hBN : (B'.subgroupOf B).Normal] (h' : A' B') (h : A B) :
                                                    A A'.subgroupOf A →* B B'.subgroupOf B

                                                    Let A', A, B', B be subgroups of G. If A' ≤ B' and A ≤ B, then there is a map A / (A' ⊓ A) →* B / (B' ⊓ B) induced by the inclusions.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem QuotientAddGroup.quotientMapAddSubgroupOfOfLe_mk {G : Type u} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} {B : AddSubgroup G} [_hAN : (A'.addSubgroupOf A).Normal] [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' B') (h : A B) (x : A) :
                                                      @[simp]
                                                      theorem QuotientGroup.quotientMapSubgroupOfOfLe_mk {G : Type u} [Group G] {A' : Subgroup G} {A : Subgroup G} {B' : Subgroup G} {B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal] [_hBN : (B'.subgroupOf B).Normal] (h' : A' B') (h : A B) (x : A) :
                                                      theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_1 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {B' : AddSubgroup G} (h' : A' = B') :
                                                      A' B'
                                                      theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_5 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} {B : AddSubgroup G} [hAN : (A'.addSubgroupOf A).Normal] [hBN : (B'.addSubgroupOf B).Normal] (h' : A' = B') (h : A = B) :
                                                      theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_6 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} {B : AddSubgroup G} [hAN : (A'.addSubgroupOf A).Normal] [hBN : (B'.addSubgroupOf B).Normal] (h' : A' = B') (h : A = B) :
                                                      def QuotientAddGroup.equivQuotientAddSubgroupOfOfEq {G : Type u} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} {B : AddSubgroup G} [hAN : (A'.addSubgroupOf A).Normal] [hBN : (B'.addSubgroupOf B).Normal] (h' : A' = B') (h : A = B) :
                                                      A A'.addSubgroupOf A ≃+ B B'.addSubgroupOf B

                                                      Let A', A, B', B be subgroups of G. If A' = B' and A = B, then the quotients A / (A' ⊓ A) and B / (B' ⊓ B) are isomorphic. Applying this equiv is nicer than rewriting along the equalities, since the type of (A'.addSubgroupOf A : AddSubgroup A) depends on A.

                                                      Equations
                                                      Instances For
                                                        theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_3 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {B' : AddSubgroup G} (h' : A' = B') :
                                                        B' A'
                                                        def QuotientGroup.equivQuotientSubgroupOfOfEq {G : Type u} [Group G] {A' : Subgroup G} {A : Subgroup G} {B' : Subgroup G} {B : Subgroup G} [hAN : (A'.subgroupOf A).Normal] [hBN : (B'.subgroupOf B).Normal] (h' : A' = B') (h : A = B) :
                                                        A A'.subgroupOf A ≃* B B'.subgroupOf B

                                                        Let A', A, B', B be subgroups of G. If A' = B' and A = B, then the quotients A / (A' ⊓ A) and B / (B' ⊓ B) are isomorphic.

                                                        Applying this equiv is nicer than rewriting along the equalities, since the type of (A'.subgroupOf A : Subgroup A) depends on A.

                                                        Equations
                                                        Instances For
                                                          def QuotientAddGroup.homQuotientZSMulOfHom {A : Type u} {B : Type u} [AddCommGroup A] [AddCommGroup B] (f : A →+ B) (n : ) :
                                                          A (zsmulAddGroupHom n).range →+ B (zsmulAddGroupHom n).range

                                                          The map of quotients by multiples of an integer induced by an additive group homomorphism.

                                                          Equations
                                                          Instances For
                                                            theorem QuotientAddGroup.homQuotientZSMulOfHom.proof_3 {A : Type u_1} {B : Type u_1} [AddCommGroup A] [AddCommGroup B] (f : A →+ B) (n : ) (g : A) :
                                                            g (zsmulAddGroupHom n).rangeg ((QuotientAddGroup.mk' (zsmulAddGroupHom n).range).comp f).ker
                                                            def QuotientGroup.homQuotientZPowOfHom {A : Type u} {B : Type u} [CommGroup A] [CommGroup B] (f : A →* B) (n : ) :
                                                            A (zpowGroupHom n).range →* B (zpowGroupHom n).range

                                                            The map of quotients by powers of an integer induced by a group homomorphism.

                                                            Equations
                                                            Instances For

                                                              The equivalence of quotients by multiples of an integer induced by an additive group isomorphism.

                                                              Equations
                                                              Instances For
                                                                def QuotientGroup.equivQuotientZPowOfEquiv {A : Type u} {B : Type u} [CommGroup A] [CommGroup B] (e : A ≃* B) (n : ) :
                                                                A (zpowGroupHom n).range ≃* B (zpowGroupHom n).range

                                                                The equivalence of quotients by powers of an integer induced by a group isomorphism.

                                                                Equations
                                                                Instances For
                                                                  theorem QuotientAddGroup.quotientInfEquivSumNormalQuotient.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (N : AddSubgroup G) [N.Normal] :
                                                                  (N.addSubgroupOf (H N)).Normal
                                                                  noncomputable def QuotientAddGroup.quotientInfEquivSumNormalQuotient {G : Type u} [AddGroup G] (H : AddSubgroup G) (N : AddSubgroup G) [N.Normal] :
                                                                  H N.addSubgroupOf H ≃+ (H N) N.addSubgroupOf (H N)

                                                                  The second isomorphism theorem: given two subgroups H and N of a group G, where N is normal, defines an isomorphism between H/(H ∩ N) and (H + N)/N

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    theorem QuotientAddGroup.quotientInfEquivSumNormalQuotient.proof_3 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (N : AddSubgroup G) [N.Normal] (x : (H N) N.addSubgroupOf (H N)) :
                                                                    ∃ (a : H), ((QuotientAddGroup.mk' (N.addSubgroupOf (H N))).comp (AddSubgroup.inclusion )) a = x
                                                                    theorem QuotientAddGroup.quotientInfEquivSumNormalQuotient.proof_5 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (N : AddSubgroup G) [N.Normal] :
                                                                    N.addSubgroupOf H = AddSubgroup.comap (AddSubgroup.inclusion ) (QuotientAddGroup.mk' (N.addSubgroupOf (H N))).ker
                                                                    theorem QuotientAddGroup.quotientInfEquivSumNormalQuotient.proof_4 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (N : AddSubgroup G) [N.Normal] :
                                                                    ((QuotientAddGroup.mk' (N.addSubgroupOf (H N))).comp (AddSubgroup.inclusion )).ker.Normal
                                                                    noncomputable def QuotientGroup.quotientInfEquivProdNormalQuotient {G : Type u} [Group G] (H : Subgroup G) (N : Subgroup G) [N.Normal] :
                                                                    H N.subgroupOf H ≃* (H N) N.subgroupOf (H N)

                                                                    Noether's second isomorphism theorem: given two subgroups H and N of a group G, where N is normal, defines an isomorphism between H/(H ∩ N) and (HN)/N.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      instance QuotientAddGroup.map_normal {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] :
                                                                      Equations
                                                                      • =
                                                                      instance QuotientGroup.map_normal {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] :
                                                                      Equations
                                                                      • =
                                                                      def QuotientAddGroup.quotientQuotientEquivQuotientAux {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N M) :

                                                                      The map from the third isomorphism theorem for additive groups: (A / N) / (M / N) → A / M.

                                                                      Equations
                                                                      Instances For
                                                                        theorem QuotientAddGroup.quotientQuotientEquivQuotientAux.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N M) :
                                                                        ∀ ⦃x : G N⦄, x AddSubgroup.map (QuotientAddGroup.mk' N) Mx (QuotientAddGroup.map N M (AddMonoidHom.id G) h).ker
                                                                        def QuotientGroup.quotientQuotientEquivQuotientAux {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N M) :

                                                                        The map from the third isomorphism theorem for groups: (G / N) / (M / N) → G / M.

                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem QuotientAddGroup.quotientQuotientEquivQuotientAux_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N M) (x : G N) :
                                                                          @[simp]
                                                                          theorem QuotientGroup.quotientQuotientEquivQuotientAux_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N M) (x : G N) :
                                                                          theorem QuotientAddGroup.quotientQuotientEquivQuotientAux_mk_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N M) (x : G) :
                                                                          theorem QuotientGroup.quotientQuotientEquivQuotientAux_mk_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N M) (x : G) :
                                                                          def QuotientAddGroup.quotientQuotientEquivQuotient {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N M) :

                                                                          Noether's third isomorphism theorem for additive groups: (A / N) / (M / N) ≃+ A / M.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            def QuotientGroup.quotientQuotientEquivQuotient {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N M) :

                                                                            Noether's third isomorphism theorem for groups: (G / N) / (M / N) ≃* G / M.

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

                                                                              If the quotient by an additive subgroup gives a singleton then the additive subgroup is the whole additive group.

                                                                              If the quotient by a subgroup gives a singleton then the subgroup is the whole group.

                                                                              @[simp]
                                                                              theorem QuotientAddGroup.mk_nat_mul {R : Type u_1} [NonAssocRing R] (N : AddSubgroup R) [N.Normal] (n : ) (a : R) :
                                                                              (n * a) = n a
                                                                              @[simp]
                                                                              theorem QuotientAddGroup.mk_int_mul {R : Type u_1} [NonAssocRing R] (N : AddSubgroup R) [N.Normal] (n : ) (a : R) :
                                                                              (n * a) = n a