isUnit_C — Mathlib

English

A constant polynomial C x is a unit in R[X] if and only if x is a unit in R.

Русский

Константный многочлен C x является единицей в R[X] тогда и только тогда, когда x является единицей в R.

LaTeX

$$$\text{IsUnit}(C x) \iff \text{IsUnit}(x).$$$

Lean4

theorem isUnit_C {x : R} : IsUnit (C x) ↔ IsUnit x :=
  ⟨fun h => (congr_arg IsUnit coeff_C_zero).mp (h.map <| @constantCoeff R _), fun h => h.map C⟩

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