fintypeOfKerEqRange — Mathlib

English

If ker of g is finite and the codomain is finite, then the domain is finite.

Русский

Если ядро g конечно и кодом конечен, тогда область определения конечна.

LaTeX

$$$[Fintype\\, g.ker] \\Rightarrow (Fintype\\, G)$$$

Lean4

/-- If `F` and `H` are finite such that `ker(G →* H) = im(F →* G)`, then `G` is finite. -/
@[to_additive /-- If `F` and `H` are finite such that `ker(G →+ H) = im(F →+ G)`, then `G` is finite. -/
    ]
noncomputable def fintypeOfKerEqRange (h : g.ker = f.range) : Fintype G :=
  fintypeOfKerLeRange _ _ h.le

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