transcendental — Mathlib

English

A polynomial f ∈ R[X] is transcendental over R if its natDegree is nonzero and its leading coefficient is not a zero divisor in R.

Русский

Полином f ∈ R[X] трансцендентен над R, если его натуральная степень не равна нулю и старший коэффициент не является нулевым делителем в R.

LaTeX

$$$ \forall {R} [\text{CommRing } R], (f : R[X]), Ne f.natDegree 0 \to f.leadingCoeff \in R^0 \to Transcendental R f $$$

Lean4

theorem transcendental (f : R[X]) (hf : f.natDegree ≠ 0) (hf' : f.leadingCoeff ∈ R⁰) : Transcendental R f := by
  simpa using (transcendental_X R).aeval f hf hf'

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