isUnit_of_coeff_zero_ne_zero — Mathlib

English

If the 0-th coefficient of a Witt vector x is nonzero, then x is a unit.

Русский

Если нулевой коэффициент вектора Витта x не равен нулю, то x является единицей.

LaTeX

$$$x.\text{coeff } 0 \neq 0 \Rightarrow IsUnit\ x$$$

Lean4

theorem isUnit_of_coeff_zero_ne_zero (x : 𝕎 k) (hx : x.coeff 0 ≠ 0) : IsUnit x :=
  by
  let y : kˣ := Units.mk0 (x.coeff 0) hx
  have hy : x.coeff 0 = y := rfl
  exact (mkUnit hy).isUnit

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