# 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 #

• mk': the canonical group homomorphism G →* G/N given a normal subgroup N of G.
• lift φ: the group homomorphism G/N →* H given a group homomorphism φ : G →* H such that N ⊆ ker φ.
• map f: the group homomorphism G/N →* H/M given a group homomorphism f : G →* H such that N ⊆ f⁻¹(M).

## Main statements #

• QuotientGroup.quotientKerEquivRange: Noether's first isomorphism theorem, an explicit isomorphism G/ker φ → range φ for every group homomorphism φ : G →* H.
• QuotientGroup.quotientInfEquivProdNormalQuotient: Noether's second isomorphism theorem, an explicit isomorphism between H/(H ∩ N) and (HN)/N given a subgroup H and a normal subgroup N of a group G.
• QuotientGroup.quotientQuotientEquivQuotient: Noether's third isomorphism theorem, the canonical isomorphism between (G / N) / (M / N) and G / M, where N ≤ M.

## Tags #

isomorphism theorems, quotient groups

def QuotientAddGroup.con {G : Type u} [] (N : ) [nN : N.Normal] :

Equations
• = { toSetoid := , add' := }
Instances For
theorem QuotientAddGroup.con.proof_1 {G : Type u_1} [] (N : ) [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} [] (N : ) [nN : N.Normal] :
Con G

The congruence relation generated by a normal subgroup.

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

The additive group homomorphism from G to G/N.

Equations
Instances For
def QuotientGroup.mk' {G : Type u} [] (N : ) [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} [] (N : ) [nN : N.Normal] :
@[simp]
theorem QuotientGroup.coe_mk' {G : Type u} [] (N : ) [nN : N.Normal] :
= QuotientGroup.mk
@[simp]
theorem QuotientAddGroup.mk'_apply {G : Type u} [] (N : ) [nN : N.Normal] (x : G) :
x = x
@[simp]
theorem QuotientGroup.mk'_apply {G : Type u} [] (N : ) [nN : N.Normal] (x : G) :
x = x
theorem QuotientAddGroup.mk'_surjective {G : Type u} [] (N : ) [nN : N.Normal] :
theorem QuotientGroup.mk'_surjective {G : Type u} [] (N : ) [nN : N.Normal] :
theorem QuotientAddGroup.mk'_eq_mk' {G : Type u} [] (N : ) [nN : N.Normal] {x : G} {y : G} :
x = y zN, x + z = y
theorem QuotientGroup.mk'_eq_mk' {G : Type u} [] (N : ) [nN : N.Normal] {x : G} {y : G} :
x = y zN, x * z = y
theorem QuotientAddGroup.sound {G : Type u} [] (N : ) [nN : N.Normal] (U : Set (G N)) (g : N.op) :
g +ᵥ ⁻¹' U = ⁻¹' U
theorem QuotientGroup.sound {G : Type u} [] (N : ) [nN : N.Normal] (U : Set (G N)) (g : N.op) :
g ⁻¹' U = ⁻¹' U
theorem QuotientAddGroup.addMonoidHom_ext {G : Type u} [] (N : ) [nN : N.Normal] {M : Type x} [] ⦃f : G N →+ M ⦃g : G N →+ M (h : f.comp = g.comp ) :
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 {G : Type u} [] (N : ) [nN : N.Normal] {M : Type x} [] ⦃f : G N →* M ⦃g : G N →* M (h : f.comp = g.comp ) :
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} [] {N : } [nN : N.Normal] (x : G) :
x = 0 x N
@[simp]
theorem QuotientGroup.eq_one_iff {G : Type u} [] {N : } [nN : N.Normal] (x : G) :
x = 1 x N
abbrev QuotientAddGroup.ker_le_range_iff.match_1 {H : Type u_1} [] {I : Type u_2} [] (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} [] {H : Type v} [] {I : Type w} [] (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} [] {H : Type v} [] {I : Type w} [] (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} [] (N : ) [nN : N.Normal] :
.ker = N
@[simp]
theorem QuotientGroup.ker_mk' {G : Type u} [] (N : ) [nN : N.Normal] :
.ker = N
theorem QuotientAddGroup.eq_iff_sub_mem {G : Type u} [] {N : } [nN : N.Normal] {x : G} {y : G} :
x = y x - y N
theorem QuotientGroup.eq_iff_div_mem {G : Type u} [] {N : } [nN : N.Normal] {x : G} {y : G} :
x = y x / y N
Equations
theorem QuotientAddGroup.Quotient.addCommGroup.proof_1 {G : Type u_1} [] (N : ) (a : G N) (b : G N) :
a + b = b + a
instance QuotientGroup.Quotient.commGroup {G : Type u_1} [] (N : ) :
Equations
@[simp]
theorem QuotientAddGroup.mk_zero {G : Type u} [] (N : ) [nN : N.Normal] :
0 = 0
@[simp]
theorem QuotientGroup.mk_one {G : Type u} [] (N : ) [nN : N.Normal] :
1 = 1
@[simp]
theorem QuotientAddGroup.mk_add {G : Type u} [] (N : ) [nN : N.Normal] (a : G) (b : G) :
(a + b) = a + b
@[simp]
theorem QuotientGroup.mk_mul {G : Type u} [] (N : ) [nN : N.Normal] (a : G) (b : G) :
(a * b) = a * b
@[simp]
theorem QuotientAddGroup.mk_neg {G : Type u} [] (N : ) [nN : N.Normal] (a : G) :
(-a) = -a
@[simp]
theorem QuotientGroup.mk_inv {G : Type u} [] (N : ) [nN : N.Normal] (a : G) :
a⁻¹ = (a)⁻¹
@[simp]
theorem QuotientAddGroup.mk_sub {G : Type u} [] (N : ) [nN : N.Normal] (a : G) (b : G) :
(a - b) = a - b
@[simp]
theorem QuotientGroup.mk_div {G : Type u} [] (N : ) [nN : N.Normal] (a : G) (b : G) :
(a / b) = a / b
@[simp]
theorem QuotientAddGroup.mk_nsmul {G : Type u} [] (N : ) [nN : N.Normal] (a : G) (n : ) :
(n a) = n a
@[simp]
theorem QuotientGroup.mk_pow {G : Type u} [] (N : ) [nN : N.Normal] (a : G) (n : ) :
(a ^ n) = a ^ n
@[simp]
theorem QuotientAddGroup.mk_zsmul {G : Type u} [] (N : ) [nN : N.Normal] (a : G) (n : ) :
(n a) = n a
@[simp]
theorem QuotientGroup.mk_zpow {G : Type u} [] (N : ) [nN : N.Normal] (a : G) (n : ) :
(a ^ n) = a ^ n
@[simp]
theorem QuotientAddGroup.mk_sum {G : Type u_1} {ι : Type u_2} [] (N : ) (s : ) {f : ιG} :
(s.sum f) = is, (f i)
@[simp]
theorem QuotientGroup.mk_prod {G : Type u_1} {ι : Type u_2} [] (N : ) (s : ) {f : ιG} :
(s.prod f) = is, (f i)
@[simp]
theorem QuotientAddGroup.map_mk'_self {G : Type u} [] (N : ) [nN : N.Normal] :
@[simp]
theorem QuotientGroup.map_mk'_self {G : Type u} [] (N : ) [nN : N.Normal] :
theorem QuotientAddGroup.lift.proof_1 {G : Type u_1} [] (N : ) [nN : N.Normal] {M : Type u_2} [] (φ : G →+ M) (HN : N φ.ker) (x : G) (y : G) (h : x y) :
() x y
def QuotientAddGroup.lift {G : Type u} [] (N : ) [nN : N.Normal] {M : Type x} [] (φ : 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
• = .lift φ
Instances For
def QuotientGroup.lift {G : Type u} [] (N : ) [nN : N.Normal] {M : Type x} [] (φ : 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
• = .lift φ
Instances For
@[simp]
theorem QuotientAddGroup.lift_mk {G : Type u} [] (N : ) [nN : N.Normal] {M : Type x} [] {φ : G →+ M} (HN : N φ.ker) (g : G) :
() g = φ g
@[simp]
theorem QuotientGroup.lift_mk {G : Type u} [] (N : ) [nN : N.Normal] {M : Type x} [] {φ : G →* M} (HN : N φ.ker) (g : G) :
() g = φ g
@[simp]
theorem QuotientAddGroup.lift_mk' {G : Type u} [] (N : ) [nN : N.Normal] {M : Type x} [] {φ : G →+ M} (HN : N φ.ker) (g : G) :
() g = φ g
@[simp]
theorem QuotientGroup.lift_mk' {G : Type u} [] (N : ) [nN : N.Normal] {M : Type x} [] {φ : G →* M} (HN : N φ.ker) (g : G) :
() g = φ g
@[simp]
theorem QuotientAddGroup.lift_quot_mk {G : Type u} [] (N : ) [nN : N.Normal] {M : Type x} [] {φ : G →+ M} (HN : N φ.ker) (g : G) :
() (Quot.mk Setoid.r g) = φ g
@[simp]
theorem QuotientGroup.lift_quot_mk {G : Type u} [] (N : ) [nN : N.Normal] {M : Type x} [] {φ : G →* M} (HN : N φ.ker) (g : G) :
() (Quot.mk Setoid.r g) = φ g
def QuotientAddGroup.map {G : Type u} [] (N : ) [nN : N.Normal] {H : Type v} [] (M : ) [M.Normal] (f : G →+ H) (h : N ) :
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} [] (N : ) {H : Type u_2} [] (M : ) (f : G →+ H) (h : N ) ⦃x : G (hx : x N) :
(f x) = 0
def QuotientGroup.map {G : Type u} [] (N : ) [nN : N.Normal] {H : Type v} [] (M : ) [M.Normal] (f : G →* H) (h : N ) :
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} [] (N : ) [nN : N.Normal] {H : Type v} [] (M : ) [M.Normal] (f : G →+ H) (h : N ) (x : G) :
() x = (f x)
@[simp]
theorem QuotientGroup.map_mk {G : Type u} [] (N : ) [nN : N.Normal] {H : Type v} [] (M : ) [M.Normal] (f : G →* H) (h : N ) (x : G) :
() x = (f x)
theorem QuotientAddGroup.map_mk' {G : Type u} [] (N : ) [nN : N.Normal] {H : Type v} [] (M : ) [M.Normal] (f : G →+ H) (h : N ) (x : G) :
() ( x) = (f x)
theorem QuotientGroup.map_mk' {G : Type u} [] (N : ) [nN : N.Normal] {H : Type v} [] (M : ) [M.Normal] (f : G →* H) (h : N ) (x : G) :
() ( x) = (f x)
theorem QuotientAddGroup.map_id_apply {G : Type u} [] (N : ) [nN : N.Normal] (h : optParam () ) (x : G N) :
() x = x
theorem QuotientGroup.map_id_apply {G : Type u} [] (N : ) [nN : N.Normal] (h : optParam (N ) ) (x : G N) :
() x = x
@[simp]
theorem QuotientAddGroup.map_id {G : Type u} [] (N : ) [nN : N.Normal] (h : optParam () ) :
@[simp]
theorem QuotientGroup.map_id {G : Type u} [] (N : ) [nN : N.Normal] (h : optParam (N ) ) :
@[simp]
theorem QuotientAddGroup.map_map {G : Type u} [] (N : ) [nN : N.Normal] {H : Type v} [] {I : Type u_1} [] (M : ) (O : ) [M.Normal] [O.Normal] (f : G →+ H) (g : H →+ I) (hf : N ) (hg : M ) (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} [] (N : ) [nN : N.Normal] {H : Type v} [] {I : Type u_1} [] (M : ) (O : ) [M.Normal] [O.Normal] (f : G →* H) (g : H →* I) (hf : N ) (hg : M ) (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} [] (N : ) [nN : N.Normal] {H : Type v} [] {I : Type u_1} [] (M : ) (O : ) [M.Normal] [O.Normal] (f : G →+ H) (g : H →+ I) (hf : N ) (hg : M ) (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} [] (N : ) [nN : N.Normal] {H : Type v} [] {I : Type u_1} [] (M : ) (O : ) [M.Normal] [O.Normal] (f : G →* H) (g : H →* I) (hf : N ) (hg : M ) (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} [] (N : ) [nN : N.Normal] :
@[simp]
theorem QuotientGroup.image_coe {G : Type u} [] (N : ) [nN : N.Normal] :
QuotientGroup.mk '' N = 1
theorem QuotientAddGroup.preimage_image_coe {G : Type u} [] (N : ) [nN : N.Normal] (s : Set G) :
theorem QuotientGroup.preimage_image_coe {G : Type u} [] (N : ) [nN : N.Normal] (s : Set G) :
QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = N * s
theorem QuotientAddGroup.image_coe_inj {G : Type u} [] (N : ) [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} [] (N : ) [nN : N.Normal] {s : Set G} {t : Set G} :
QuotientGroup.mk '' s = QuotientGroup.mk '' t N * s = N * t
theorem QuotientAddGroup.congr.proof_3 {G : Type u_1} [] {H : Type u_2} [] (G' : ) (H' : ) (e : G ≃+ H) (he : AddSubgroup.map (e) G' = H') :
def QuotientAddGroup.congr {G : Type u} [] {H : Type v} [] (G' : ) (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_7 {G : Type u_2} [] {H : Type u_1} [] (G' : ) (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} [] {H : Type u_1} [] (G' : ) (H' : ) (e : G ≃+ H) (he : AddSubgroup.map (e) G' = H') :
theorem QuotientAddGroup.congr.proof_1 {G : Type u_1} [] {H : Type u_2} [] :
theorem QuotientAddGroup.congr.proof_8 {G : Type u_1} [] {H : Type u_2} [] (G' : ) (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_6 {G : Type u_1} [] {H : Type u_2} [] (G' : ) (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_2 {G : Type u_1} [] {H : Type u_2} [] (G' : ) (H' : ) (e : G ≃+ H) (he : AddSubgroup.map (e) G' = H') :
theorem QuotientAddGroup.congr.proof_4 {G : Type u_1} [] {H : Type u_2} [] :
def QuotientGroup.congr {G : Type u} [] {H : Type v} [] (G' : ) (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} [] {H : Type v} [] (G' : ) (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} [] {H : Type v} [] (G' : ) (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)
@[simp]
theorem QuotientGroup.congr_apply {G : Type u} [] {H : Type v} [] (G' : ) (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)
@[simp]
theorem QuotientGroup.congr_refl {G : Type u} [] (G' : ) [G'.Normal] (he : optParam (Subgroup.map (()) G' = G') ) :
@[simp]
theorem QuotientGroup.congr_symm {G : Type u} [] {H : Type v} [] (G' : ) (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} [] {H : Type v} [] (φ : G →+ H) :
G φ.ker →+ H

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

Equations
Instances For
theorem QuotientAddGroup.kerLift.proof_1 {G : Type u_1} [] {H : Type u_2} [] (φ : G →+ H) :
φ.ker.Normal
theorem QuotientAddGroup.kerLift.proof_2 {G : Type u_1} [] {H : Type u_2} [] (φ : G →+ H) (_g : G) :
_g φ.kerφ _g = 0
def QuotientGroup.kerLift {G : Type u} [] {H : Type v} [] (φ : 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} [] {H : Type v} [] (φ : G →+ H) (g : G) :
g = φ g
@[simp]
theorem QuotientGroup.kerLift_mk {G : Type u} [] {H : Type v} [] (φ : G →* H) (g : G) :
g = φ g
@[simp]
theorem QuotientAddGroup.kerLift_mk' {G : Type u} [] {H : Type v} [] (φ : G →+ H) (g : G) :
g = φ g
@[simp]
theorem QuotientGroup.kerLift_mk' {G : Type u} [] {H : Type v} [] (φ : G →* H) (g : G) :
g = φ g
theorem QuotientAddGroup.kerLift_injective {G : Type u} [] {H : Type v} [] (φ : G →+ H) :
theorem QuotientGroup.kerLift_injective {G : Type u} [] {H : Type v} [] (φ : G →* H) :
def QuotientAddGroup.rangeKerLift {G : Type u} [] {H : Type v} [] (φ : G →+ H) :
G φ.ker →+ φ.range

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

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

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

Equations
Instances For
theorem QuotientAddGroup.rangeKerLift_injective {G : Type u} [] {H : Type v} [] (φ : G →+ H) :
theorem QuotientGroup.rangeKerLift_injective {G : Type u} [] {H : Type v} [] (φ : G →* H) :
theorem QuotientAddGroup.rangeKerLift_surjective {G : Type u} [] {H : Type v} [] (φ : G →+ H) :
theorem QuotientGroup.rangeKerLift_surjective {G : Type u} [] {H : Type v} [] (φ : G →* H) :
theorem QuotientAddGroup.quotientKerEquivRange.proof_3 {G : Type u_1} [] {H : Type u_2} [] (φ : G →+ H) :
noncomputable def QuotientAddGroup.quotientKerEquivRange {G : Type u} [] {H : Type v} [] (φ : G →+ H) :
G φ.ker ≃+ φ.range

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

Equations
Instances For
theorem QuotientAddGroup.quotientKerEquivRange.proof_2 {G : Type u_1} [] {H : Type u_2} [] (φ : G →+ H) :
AddHomClass (G φ.ker →+ φ.range) (G φ.ker) φ.range
theorem QuotientAddGroup.quotientKerEquivRange.proof_1 {G : Type u_1} [] {H : Type u_2} [] (φ : G →+ H) :
φ.ker.Normal
noncomputable def QuotientGroup.quotientKerEquivRange {G : Type u} [] {H : Type v} [] (φ : 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_3 {G : Type u_1} [] {H : Type u_2} [] (φ : G →+ H) (x : G φ.ker) (y : G φ.ker) :
().toFun (x + y) = ().toFun x + ().toFun y
theorem QuotientAddGroup.quotientKerEquivOfRightInverse.proof_2 {G : Type u_1} [] {H : Type u_2} [] (φ : G →+ H) (ψ : HG) (hφ : ) (x : G φ.ker) :
def QuotientAddGroup.quotientKerEquivOfRightInverse {G : Type u} [] {H : Type v} [] (φ : G →+ H) (ψ : HG) (hφ : ) :
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} [] {H : Type u_2} [] (φ : G →+ H) :
φ.ker.Normal
@[simp]
theorem QuotientAddGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [] {H : Type v} [] (φ : G →+ H) (ψ : HG) (hφ : ) (a : G φ.ker) :
@[simp]
theorem QuotientAddGroup.quotientKerEquivOfRightInverse_symm_apply {G : Type u} [] {H : Type v} [] (φ : G →+ H) (ψ : HG) (hφ : ) :
∀ (a : H), .symm a = (QuotientAddGroup.mk ψ) a
@[simp]
theorem QuotientGroup.quotientKerEquivOfRightInverse_symm_apply {G : Type u} [] {H : Type v} [] (φ : G →* H) (ψ : HG) (hφ : ) :
∀ (a : H), .symm a = (QuotientGroup.mk ψ) a
@[simp]
theorem QuotientGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [] {H : Type v} [] (φ : G →* H) (ψ : HG) (hφ : ) (a : G φ.ker) :
=
def QuotientGroup.quotientKerEquivOfRightInverse {G : Type u} [] {H : Type v} [] (φ : G →* H) (ψ : HG) (hφ : ) :
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.quotientBot.proof_1 {G : Type u_1} [] (_x : G) :
() (id _x) = () (id _x)

The canonical isomorphism G/⊥ ≃+ G.

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

The canonical isomorphism G/⊥ ≃* G.

Equations
• QuotientGroup.quotientBot =
Instances For
theorem QuotientAddGroup.quotientKerEquivOfSurjective.proof_1 {G : Type u_1} [] {H : Type u_2} [] (φ : G →+ H) (hφ : ) :
theorem QuotientAddGroup.quotientKerEquivOfSurjective.proof_2 {G : Type u_1} [] {H : Type u_2} [] (φ : G →+ H) (hφ : ) :
noncomputable def QuotientAddGroup.quotientKerEquivOfSurjective {G : Type u} [] {H : Type v} [] (φ : G →+ H) (hφ : ) :
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} [] {H : Type v} [] (φ : G →* H) (hφ : ) :
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
theorem QuotientAddGroup.quotientAddEquivOfEq.proof_1 {G : Type u_1} [] {M : } {N : } [M.Normal] [N.Normal] (h : M = N) (q : G M) (r : G M) :
.toFun (q + r) = .toFun q + .toFun r
def QuotientAddGroup.quotientAddEquivOfEq {G : Type u} [] {M : } {N : } [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
• = let __src := ; { toEquiv := __src, map_add' := }
Instances For
def QuotientGroup.quotientMulEquivOfEq {G : Type u} [] {M : } {N : } [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
• = let __src := ; { toEquiv := __src, map_mul' := }
Instances For
@[simp]
theorem QuotientAddGroup.quotientAddEquivOfEq_mk {G : Type u} [] {M : } {N : } [M.Normal] [N.Normal] (h : M = N) (x : G) :
@[simp]
theorem QuotientGroup.quotientMulEquivOfEq_mk {G : Type u} [] {M : } {N : } [M.Normal] [N.Normal] (h : M = N) (x : G) :
= x
theorem QuotientAddGroup.quotientMapAddSubgroupOfOfLe.proof_1 {G : Type u_1} [] {A' : } {A : } {B' : } (h' : A' B') :
def QuotientAddGroup.quotientMapAddSubgroupOfOfLe {G : Type u} [] {A' : } {A : } {B' : } {B : } [_hAN : (A'.addSubgroupOf A).Normal] [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' B') (h : A 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
def QuotientGroup.quotientMapSubgroupOfOfLe {G : Type u} [] {A' : } {A : } {B' : } {B : } [_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} [] {A' : } {A : } {B' : } {B : } [_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} [] {A' : } {A : } {B' : } {B : } [_hAN : (A'.subgroupOf A).Normal] [_hBN : (B'.subgroupOf B).Normal] (h' : A' B') (h : A B) (x : A) :
= ( x)
theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_2 {G : Type u_1} [] {A : } {B : } (h : A = B) :
A B
theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_3 {G : Type u_1} [] {A' : } {B' : } (h' : A' = B') :
B' A'
theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_1 {G : Type u_1} [] {A' : } {B' : } (h' : A' = B') :
A' B'
def QuotientAddGroup.equivQuotientAddSubgroupOfOfEq {G : Type u} [] {A' : } {A : } {B' : } {B : } [hAN : (A'.addSubgroupOf A).Normal] [hBN : (B'.addSubgroupOf B).Normal] (h' : A' = B') (h : A = 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} [] {A' : } {A : } {B' : } {B : } [hAN : (A'.addSubgroupOf A).Normal] [hBN : (B'.addSubgroupOf B).Normal] (h' : A' = B') (h : A = B) :
theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_5 {G : Type u_1} [] {A' : } {A : } {B' : } {B : } [hAN : (A'.addSubgroupOf A).Normal] [hBN : (B'.addSubgroupOf B).Normal] (h' : A' = B') (h : A = B) :
theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_4 {G : Type u_1} [] {A : } {B : } (h : A = B) :
B A
def QuotientGroup.equivQuotientSubgroupOfOfEq {G : Type u} [] {A' : } {A : } {B' : } {B : } [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
• = .toMulEquiv
Instances For
theorem QuotientAddGroup.homQuotientZSMulOfHom.proof_1 {A : Type u_1} [] (n : ) :
().range.Normal
abbrev QuotientAddGroup.homQuotientZSMulOfHom.match_1 {A : Type u_1} [] (n : ) (g : A) (motive : g ().rangeProp) :
∀ (x : g ().range), (∀ (h : A) (hg : n h = g), motive )motive x
Equations
• =
Instances For
theorem QuotientAddGroup.homQuotientZSMulOfHom.proof_2 {B : Type u_1} [] (n : ) :
().range.Normal
def QuotientAddGroup.homQuotientZSMulOfHom {A : Type u} {B : Type u} [] [] (f : A →+ B) (n : ) :
A ().range →+ B ().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} [] [] (f : A →+ B) (n : ) (g : A) :
def QuotientGroup.homQuotientZPowOfHom {A : Type u} {B : Type u} [] [] (f : A →* B) (n : ) :
A ().range →* B ().range

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

Equations
Instances For
@[simp]
theorem QuotientAddGroup.homQuotientZSMulOfHom_id {A : Type u} [] (n : ) :
@[simp]
theorem QuotientGroup.homQuotientZPowOfHom_id {A : Type u} [] (n : ) :
= MonoidHom.id (A ().range)
@[simp]
theorem QuotientAddGroup.homQuotientZSMulOfHom_comp {A : Type u} {B : Type u} [] [] (f : A →+ B) (g : B →+ A) (n : ) :
@[simp]
theorem QuotientGroup.homQuotientZPowOfHom_comp {A : Type u} {B : Type u} [] [] (f : A →* B) (g : B →* A) (n : ) :
@[simp]
theorem QuotientAddGroup.homQuotientZSMulOfHom_comp_of_rightInverse {A : Type u} {B : Type u} [] [] (f : A →+ B) (g : B →+ A) (n : ) (i : ) :
@[simp]
theorem QuotientGroup.homQuotientZPowOfHom_comp_of_rightInverse {A : Type u} {B : Type u} [] [] (f : A →* B) (g : B →* A) (n : ) (i : ) :
.comp = MonoidHom.id (B ().range)
def QuotientAddGroup.equivQuotientZSMulOfEquiv {A : Type u} {B : Type u} [] [] (e : A ≃+ B) (n : ) :
A ().range ≃+ B ().range

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

Equations
Instances For
theorem QuotientAddGroup.equivQuotientZSMulOfEquiv.proof_2 {B : Type u_1} [] (n : ) :
().range.Normal
theorem QuotientAddGroup.equivQuotientZSMulOfEquiv.proof_1 {A : Type u_1} [] (n : ) :
().range.Normal
theorem QuotientAddGroup.equivQuotientZSMulOfEquiv.proof_5 {A : Type u_1} {B : Type u_1} [] [] (e : A ≃+ B) (n : ) :
theorem QuotientAddGroup.equivQuotientZSMulOfEquiv.proof_6 {A : Type u_1} {B : Type u_1} [] [] (e : A ≃+ B) (n : ) :
def QuotientGroup.equivQuotientZPowOfEquiv {A : Type u} {B : Type u} [] [] (e : A ≃* B) (n : ) :
A ().range ≃* B ().range

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

Equations
Instances For
@[simp]
@[simp]
theorem QuotientGroup.equivQuotientZPowOfEquiv_refl {A : Type u} [] (n : ) :
MulEquiv.refl (A ().range) =
@[simp]
theorem QuotientAddGroup.equivQuotientZSMulOfEquiv_symm {A : Type u} {B : Type u} [] [] (e : A ≃+ B) (n : ) :
@[simp]
theorem QuotientGroup.equivQuotientZPowOfEquiv_symm {A : Type u} {B : Type u} [] [] (e : A ≃* B) (n : ) :
.symm =
@[simp]
theorem QuotientAddGroup.equivQuotientZSMulOfEquiv_trans {A : Type u} {B : Type u} {C : Type u} [] [] [] (e : A ≃+ B) (d : B ≃+ C) (n : ) :
@[simp]
theorem QuotientGroup.equivQuotientZPowOfEquiv_trans {A : Type u} {B : Type u} {C : Type u} [] [] [] (e : A ≃* B) (d : B ≃* C) (n : ) :
theorem QuotientAddGroup.quotientInfEquivSumNormalQuotient.proof_1 {G : Type u_1} [] (H : ) (N : ) [N.Normal] :
theorem QuotientAddGroup.quotientInfEquivSumNormalQuotient.proof_3 {G : Type u_1} [] (H : ) (N : ) [N.Normal] (x : (H N) N.addSubgroupOf (H N)) :
∃ (a : H), ((QuotientAddGroup.mk' (N.addSubgroupOf (H N))).comp ) a = x
noncomputable def QuotientAddGroup.quotientInfEquivSumNormalQuotient {G : Type u} [] (H : ) (N : ) [N.Normal] :

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_5 {G : Type u_1} [] (H : ) (N : ) [N.Normal] :
theorem QuotientAddGroup.quotientInfEquivSumNormalQuotient.proof_4 {G : Type u_1} [] (H : ) (N : ) [N.Normal] :
noncomputable def QuotientGroup.quotientInfEquivProdNormalQuotient {G : Type u} [] (H : ) (N : ) [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} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] :
().Normal
Equations
• =
instance QuotientGroup.map_normal {G : Type u} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] :
().Normal
Equations
• =
def QuotientAddGroup.quotientQuotientEquivQuotientAux {G : Type u} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] (h : N M) :
(G N) →+ G 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} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] (h : N M) :
∀ ⦃x : G N⦄, x ().ker
def QuotientGroup.quotientQuotientEquivQuotientAux {G : Type u} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] (h : N M) :
(G N) →* G 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} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] (h : N M) (x : G N) :
= () x
@[simp]
theorem QuotientGroup.quotientQuotientEquivQuotientAux_mk {G : Type u} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] (h : N M) (x : G N) :
= () x
theorem QuotientAddGroup.quotientQuotientEquivQuotientAux_mk_mk {G : Type u} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] (h : N M) (x : G) :
= x
theorem QuotientGroup.quotientQuotientEquivQuotientAux_mk_mk {G : Type u} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] (h : N M) (x : G) :
= x
def QuotientAddGroup.quotientQuotientEquivQuotient {G : Type u} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] (h : N M) :
(G N) ≃+ G 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
theorem QuotientAddGroup.quotientQuotientEquivQuotient.proof_3 {G : Type u_1} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] (h : N M) :
.comp () = AddMonoidHom.id (G M)
theorem QuotientAddGroup.quotientQuotientEquivQuotient.proof_1 {G : Type u_1} [] (N : ) [nN : N.Normal] (M : ) :
theorem QuotientAddGroup.quotientQuotientEquivQuotient.proof_2 {G : Type u_1} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] (h : N M) :
().comp = AddMonoidHom.id ((G N) )
def QuotientGroup.quotientQuotientEquivQuotient {G : Type u} [] (N : ) [nN : N.Normal] (M : ) [nM : M.Normal] (h : N M) :
(G N) ≃* G 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.

theorem QuotientGroup.subgroup_eq_top_of_subsingleton {G : Type u} [] (H : ) (h : Subsingleton (G H)) :
H =

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

theorem QuotientAddGroup.comap_comap_center {G : Type u} [] {H₁ : } [H₁.Normal] {H₂ : AddSubgroup (G H₁)} [H₂.Normal] :
theorem QuotientGroup.comap_comap_center {G : Type u} [] {H₁ : } [H₁.Normal] {H₂ : Subgroup (G H₁)} [H₂.Normal] :
theorem AddGroup.fintypeOfKerLeRange.proof_2 {F : Type u_1} {G : Type u_1} {H : Type u_1} [] [] [] (f : F →+ G) (g : G →+ H) (h : g.ker f.range) :
theorem AddGroup.fintypeOfKerLeRange.proof_1 {G : Type u_1} {H : Type u_1} [] [] (g : G →+ H) :
g.ker.Normal
noncomputable def AddGroup.fintypeOfKerLeRange {F : Type u} {G : Type u} {H : Type u} [] [] [] [] [] (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 Group.fintypeOfKerLeRange {F : Type u} {G : Type u} {H : Type u} [] [] [] [] [] (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} [] [] [] (f : F →+ G) (g : G →+ H) (h : g.ker = f.range) :
g.ker f.range
noncomputable def AddGroup.fintypeOfKerEqRange {F : Type u} {G : Type u} {H : Type u} [] [] [] [] [] (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 Group.fintypeOfKerEqRange {F : Type u} {G : Type u} {H : Type u} [] [] [] [] [] (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_2 {G : Type u_1} {H : Type u_1} [] [] (g : G →+ H) (x : G) (hx : x g.ker) :
noncomputable def AddGroup.fintypeOfKerOfCodom {G : Type u} {H : Type u} [] [] [] (g : G →+ H) [Fintype g.ker] :

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

Equations
Instances For
theorem AddGroup.fintypeOfKerOfCodom.proof_1 {G : Type u_1} {H : Type u_1} [] [] (g : G →+ H) :
g.ker
noncomputable def Group.fintypeOfKerOfCodom {G : Type u} {H : Type u} [] [] [] (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} [] [] (f : F →+ G) [f.range.Normal] (x : G) :
x = 0x f.range
noncomputable def AddGroup.fintypeOfDomOfCoker {F : Type u} {G : Type u} [] [] [] (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} [] [] [] (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