not_separable_zero — Mathlib

English

Let R be a nontrivial commutative semiring. Then the zero polynomial in R[X] is not separable.

Русский

Пусть R — непорожденное коммутативное полукольцо. Тот нулевой многочлен в R[X] неразделим.

LaTeX

$$$[\\text{Nontrivial } R] \\\\Rightarrow \\\\neg \operatorname{Separable}(0 : R[X])$$$

Lean4

theorem not_separable_zero [Nontrivial R] : ¬Separable (0 : R[X]) :=
  by
  rintro ⟨x, y, h⟩
  simp only [derivative_zero, mul_zero, add_zero, zero_ne_one] at h

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