Deducing finiteness of a group.

noncomputable def Group.fintypeOfKerLeRange {F : Type u_1} {G : Type u_2} {H : Type u_3} [Group F] [Group G] [Group H] [Fintype F] [Fintype H] (f : F →* G) (g : G →* H) (h : g.ker ≤ f.range) : Fintype G

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

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

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

noncomputable def Group.fintypeOfKerEqRange {F : Type u_1} {G : Type u_2} {H : Type u_3} [Group F] [Group G] [Group H] [Fintype F] [Fintype H] (f : F →* G) (g : G →* H) (h : g.ker = f.range) : Fintype G

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

noncomputable def AddGroup.fintypeOfKerEqRange {F : Type u_1} {G : Type u_2} {H : Type u_3} [AddGroup F] [AddGroup G] [AddGroup H] [Fintype F] [Fintype H] (f : F →+ G) (g : G →+ H) (h : g.ker = f.range) : Fintype G

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

noncomputable def Group.fintypeOfKerOfCodom {G : Type u_2} {H : Type u_3} [Group G] [Group H] [Fintype H] (g : G →* H) [Fintype ↥g.ker] : Fintype G

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

noncomputable def AddGroup.fintypeOfKerOfCodom {G : Type u_2} {H : Type u_3} [AddGroup G] [AddGroup H] [Fintype H] (g : G →+ H) [Fintype ↥g.ker] : Fintype G

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

noncomputable def Group.fintypeOfDomOfCoker {F : Type u_1} {G : Type u_2} [Group F] [Group G] [Fintype F] (f : F →* G) [f.range.Normal] [Fintype (G ⧸ f.range)] : Fintype G

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

noncomputable def AddGroup.fintypeOfDomOfCoker {F : Type u_1} {G : Type u_2} [AddGroup F] [AddGroup G] [Fintype F] (f : F →+ G) [f.range.Normal] [Fintype (G ⧸ f.range)] : Fintype G

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

theorem finite_iff_subgroup_quotient {G : Type u_2} [Group G] (H : Subgroup G) : Finite G ↔ Finite ↥H ∧ Finite (G ⧸ H)

theorem finite_iff_addSubgroup_quotient {G : Type u_2} [AddGroup G] (H : AddSubgroup G) : Finite G ↔ Finite ↥H ∧ Finite (G ⧸ H)

theorem Finite.of_subgroup_quotient {G : Type u_2} [Group G] (H : Subgroup G) [Finite ↥H] [Finite (G ⧸ H)] : Finite G

theorem Finite.of_addSubgroup_quotient {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [Finite ↥H] [Finite (G ⧸ H)] : Finite G

@[deprecated Finite.of_subgroup_quotient (since := "2025-11-11")]

theorem Finite.of_finite_quot_finite_subgroup {G : Type u_2} [Group G] (H : Subgroup G) [Finite ↥H] [Finite (G ⧸ H)] : Finite G

Alias of Finite.of_subgroup_quotient.

@[deprecated Finite.of_addSubgroup_quotient (since := "2025-11-11")]

theorem Finite.of_finite_quot_finite_addSubgroup {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [Finite ↥H] [Finite (G ⧸ H)] : Finite G

Alias of Finite.of_addSubgroup_quotient.