not_irreducible_C — Mathlib

English

For any x in R, the constant polynomial C(x) is not irreducible: if x ≠ 0 it is a unit; if x = 0 it is zero.

Русский

Для любого x в R константный полином C(x) не неприводим: если x ≠ 0, то он единица; если x = 0, то это ноль.

LaTeX

$$not Irreducible (C x) for all x ∈ R$$

Lean4

theorem not_irreducible_C (x : R) : ¬Irreducible (C x) :=
  by
  by_cases H : x = 0
  · rw [H, C_0]
    exact not_irreducible_zero
  · exact fun hx => hx.not_isUnit <| isUnit_C.2 <| isUnit_iff_ne_zero.2 H

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