prime_X_sub_C — Mathlib

English

Let R be a commutative domain. Then for every r ∈ R, the polynomial X − r is a prime element of R[X].

Русский

Пусть R — коммутативное кольцо без делителей нуля. Тогда для любого r ∈ R многочлен X − r над R[X] является простым элементом.

LaTeX

$$$\forall r \in R,\; X - C r \text{ is prime in } R[X].$$$

Lean4

theorem prime_X_sub_C (r : R) : Prime (X - C r) :=
  ⟨X_sub_C_ne_zero r, not_isUnit_X_sub_C r, fun _ _ =>
    by
    simp_rw [dvd_iff_isRoot, IsRoot.def, eval_mul, mul_eq_zero]
    exact id⟩

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