finite_iff_finite_ker_range — Mathlib

English

For a group homomorphism f: G →* G', G is finite if and only if ker f is finite and range f is finite.

Русский

Пусть f: G →* G' — гомоморфизм. Тогда G конечно тогда, когда ядро f конечно и образ f конечно.

LaTeX

$$$|G| < \infty \iff (|\ker f| < \infty \land |f(G)| < \infty)$$$

Lean4

@[to_additive]
theorem _root_.MonoidHom.finite_iff_finite_ker_range (f : G →* G') : Finite G ↔ Finite f.ker ∧ Finite f.range := by
  rw [finite_iff_finite_and_finiteIndex f.ker, ← (QuotientGroup.quotientKerEquivRange f).finite_iff,
    finiteIndex_iff_finite_quotient]

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