fintypeOfDomOfCoker — Mathlib

English

If F and the cokernel F →* G are finite, then G is finite.

Русский

Если F и кофактор F →* G конечны, то G конечна.

LaTeX

$$$\\text{Fintype}(F) \\land \\text{Fintype}(\\text{HasQuotient.Quotient } G\\, f.range) \\Rightarrow \\text{Fintype}(G)$$$

Lean4

/-- If `F` and `coker(F →* G)` are finite, then `G` is finite. -/
@[to_additive /-- If `F` and `coker(F →+ G)` are finite, then `G` is finite. -/
    ]
noncomputable def fintypeOfDomOfCoker [Normal f.range] [Fintype <| G ⧸ f.range] : Fintype G :=
  fintypeOfKerLeRange _ (mk' f.range) fun x => (eq_one_iff x).mp

Похожие утверждения