fintypeOfKerOfCodom — Mathlib

English

A variant ensuring finiteness under a different presentation of the codomain.

Русский

Вариант с другой формой кодома, сохраняющий конечность ядра.

LaTeX

$$$Fintype (Subtype \\{ x \\mid g.ker x \\}) \\Rightarrow Fintype G$$$

Lean4

/-- If `ker(G →* H)` and `H` are finite, then `G` is finite. -/
@[to_additive /-- If `ker(G →+ H)` and `H` are finite, then `G` is finite. -/
    ]
noncomputable def fintypeOfKerOfCodom [Fintype g.ker] : Fintype G :=
  fintypeOfKerLeRange ((topEquiv : _ ≃* G).toMonoidHom.comp <| inclusion le_top) g fun x hx => ⟨⟨x, hx⟩, rfl⟩

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