Documentation

Mathlib.GroupTheory.QuotientGroup

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

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
    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 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
          @[inline]
          abbrev QuotientAddGroup.ker_le_range_iff.match_1 {H : Type u_1} [AddGroup H] {I : Type u_2} [AddGroup I] (g : H →+ I) (motive : g.kerProp) :
          ∀ (x : g.ker), (∀ (val : H) (hx : val g.ker), motive val, hx)motive x
          Equations
          • =
          Instances For
            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] :
            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 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
              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
                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
                  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 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
                    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
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      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_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_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_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
                      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'
                      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
                      • One or more equations did not get rendered due to their size.
                      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
                        theorem QuotientAddGroup.kerLift.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) :
                        φ.ker.Normal
                        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
                        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
                          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_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
                              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
                              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
                                    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
                                    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
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem QuotientAddGroup.quotientKerEquivOfRightInverse.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) :
                                      φ.ker.Normal
                                      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
                                      @[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 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 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
                                      @[simp]
                                      theorem QuotientGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : HG) (hφ : Function.RightInverse ψ φ) (a : G φ.ker) :
                                      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
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        The canonical isomorphism G/⊥ ≃+ G.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem QuotientAddGroup.quotientBot_symm_apply {G : Type u} [AddGroup G] :
                                          ∀ (a : G), QuotientAddGroup.quotientBot.symm a = 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
                                          @[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_symm_apply {G : Type u} [Group G] :
                                          ∀ (a : G), QuotientGroup.quotientBot.symm a = 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_3 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {B' : AddSubgroup G} (h' : A' = B') :
                                                        B' A'
                                                        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) :
                                                        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 on A.

                                                        Equations
                                                        Instances For
                                                          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 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
                                                              @[inline]
                                                              abbrev QuotientAddGroup.homQuotientZSMulOfHom.match_1 {A : Type u_1} [AddCommGroup A] (n : ) (g : A) (motive : g (zsmulAddGroupHom n).rangeProp) :
                                                              ∀ (x : g (zsmulAddGroupHom n).range), (∀ (h : A) (hg : n h = g), motive )motive x
                                                              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
                                                                      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
                                                                      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
                                                                      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
                                                                        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.

                                                                                  theorem AddGroup.fintypeOfKerLeRange.proof_2 {F : Type u_1} {G : Type u_1} {H : Type u_1} [AddGroup F] [AddGroup G] [AddGroup H] (f : F →+ G) (g : G →+ H) (h : g.ker f.range) :
                                                                                  noncomputable def AddGroup.fintypeOfKerLeRange {F : Type u} {G : Type u} {H : Type u} [AddGroup F] [AddGroup G] [AddGroup H] [Fintype F] [Fintype H] (f : F →+ G) (g : G →+ H) (h : g.ker f.range) :

                                                                                  If F and H are finite such that ker(G →+ H) ≤ im(F →+ G), then G is finite.

                                                                                  Equations
                                                                                  Instances For
                                                                                    theorem AddGroup.fintypeOfKerLeRange.proof_1 {G : Type u_1} {H : Type u_1} [AddGroup G] [AddGroup H] (g : G →+ H) :
                                                                                    g.ker.Normal
                                                                                    noncomputable def Group.fintypeOfKerLeRange {F : Type u} {G : Type u} {H : Type u} [Group F] [Group G] [Group H] [Fintype F] [Fintype H] (f : F →* G) (g : G →* H) (h : g.ker f.range) :

                                                                                    If F and H are finite such that ker(G →* H) ≤ im(F →* G), then G is finite.

                                                                                    Equations
                                                                                    Instances For
                                                                                      noncomputable def AddGroup.fintypeOfKerEqRange {F : Type u} {G : Type u} {H : Type u} [AddGroup F] [AddGroup G] [AddGroup H] [Fintype F] [Fintype H] (f : F →+ G) (g : G →+ H) (h : g.ker = f.range) :

                                                                                      If F and H are finite such that ker(G →+ H) = im(F →+ G), then G is finite.

                                                                                      Equations
                                                                                      Instances For
                                                                                        theorem AddGroup.fintypeOfKerEqRange.proof_1 {F : Type u_1} {G : Type u_1} {H : Type u_1} [AddGroup F] [AddGroup G] [AddGroup H] (f : F →+ G) (g : G →+ H) (h : g.ker = f.range) :
                                                                                        g.ker f.range
                                                                                        noncomputable def Group.fintypeOfKerEqRange {F : Type u} {G : Type u} {H : Type u} [Group F] [Group G] [Group H] [Fintype F] [Fintype H] (f : F →* G) (g : G →* H) (h : g.ker = f.range) :

                                                                                        If F and H are finite such that ker(G →* H) = im(F →* G), then G is finite.

                                                                                        Equations
                                                                                        Instances For
                                                                                          theorem AddGroup.fintypeOfKerOfCodom.proof_1 {G : Type u_1} {H : Type u_1} [AddGroup G] [AddGroup H] (g : G →+ H) :
                                                                                          g.ker
                                                                                          theorem AddGroup.fintypeOfKerOfCodom.proof_2 {G : Type u_1} {H : Type u_1} [AddGroup G] [AddGroup H] (g : G →+ H) (x : G) (hx : x g.ker) :
                                                                                          ∃ (y : g.ker), (AddSubgroup.topEquiv.toAddMonoidHom.comp (AddSubgroup.inclusion )) y = x
                                                                                          noncomputable def AddGroup.fintypeOfKerOfCodom {G : Type u} {H : Type u} [AddGroup G] [AddGroup H] [Fintype H] (g : G →+ H) [Fintype g.ker] :

                                                                                          If ker(G →+ H) and H are finite, then G is finite.

                                                                                          Equations
                                                                                          Instances For
                                                                                            noncomputable def Group.fintypeOfKerOfCodom {G : Type u} {H : Type u} [Group G] [Group H] [Fintype H] (g : G →* H) [Fintype g.ker] :

                                                                                            If ker(G →* H) and H are finite, then G is finite.

                                                                                            Equations
                                                                                            Instances For
                                                                                              theorem AddGroup.fintypeOfDomOfCoker.proof_1 {F : Type u_1} {G : Type u_1} [AddGroup F] [AddGroup G] (f : F →+ G) [f.range.Normal] (x : G) :
                                                                                              x = 0x f.range
                                                                                              noncomputable def AddGroup.fintypeOfDomOfCoker {F : Type u} {G : Type u} [AddGroup F] [AddGroup G] [Fintype F] (f : F →+ G) [f.range.Normal] [Fintype (G f.range)] :

                                                                                              If F and coker(F →+ G) are finite, then G is finite.

                                                                                              Equations
                                                                                              Instances For
                                                                                                noncomputable def Group.fintypeOfDomOfCoker {F : Type u} {G : Type u} [Group F] [Group G] [Fintype F] (f : F →* G) [f.range.Normal] [Fintype (G f.range)] :

                                                                                                If F and coker(F →* G) are finite, then G is finite.

                                                                                                Equations
                                                                                                Instances For