ker_isPrime — Mathlib

English

The kernel of a homomorphism to a domain is a prime ideal.

Русский

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

LaTeX

$$$(\\ker f).IsPrime$$

Lean4

/-- The kernel of a homomorphism to a domain is a prime ideal. -/
theorem ker_isPrime {F : Type*} [Semiring R] [Semiring S] [IsDomain S] [FunLike F R S] [RingHomClass F R S] (f : F) :
    (ker f).IsPrime :=
  have := Ideal.bot_prime (α := S)
  inferInstanceAs (Ideal.comap f ⊥).IsPrime

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