coeff_coe_units_zero_ne_zero — Mathlib

English

For a nontrivial ring R, the constant term of any unit in Polynomial R is nonzero.

Русский

Для ненулевого кольца R константный член любой единицы полинома не равен нулю.

LaTeX

$$$\mathrm{coeff}(u,0) \neq 0$$$

Lean4

theorem coeff_coe_units_zero_ne_zero [Nontrivial R] (u : R[X]ˣ) : coeff (u : R[X]) 0 ≠ 0 :=
  by
  conv in 0 => rw [← natDegree_coe_units u]
  rw [← leadingCoeff, Ne, leadingCoeff_eq_zero]
  exact Units.ne_zero _

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