ker_isMaximal_of_surjective — Mathlib

English

The kernel of a homomorphism onto a field is a maximal ideal.

Русский

Ядро гомоморфизма, достигающего поля, является максимальным идеалом.

LaTeX

$$If f is surjective to a field K, then ker f is maximal in R.$$

Lean4

/-- The kernel of a homomorphism to a field is a maximal ideal. -/
theorem ker_isMaximal_of_surjective {R K F : Type*} [Ring R] [DivisionRing K] [FunLike F R K] [RingHomClass F R K]
    (f : F) (hf : Function.Surjective f) : (ker f).IsMaximal :=
  have := Ideal.bot_isMaximal (K := K)
  Ideal.comap_isMaximal_of_surjective _ hf

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