isUnit_iff_eq_C_of_isReduced — Mathlib

English

If R is reduced, a unit P in MvPolynomial σ R is exactly a constant polynomial C r with r a unit.

Русский

Если R редуцировано, то единица в MvPolynomial σ R есть ровно константный многочлен C r с r единицей кольца.

LaTeX

$$$$ [IsReduced(R)] \\Rightarrow \\operatorname{IsUnit}(P) \\iff \\exists r, \\operatorname{IsUnit}(r) \\wedge P = C r. $$$$

Lean4

theorem isUnit_iff_eq_C_of_isReduced [IsReduced R] : IsUnit P ↔ ∃ r, IsUnit r ∧ P = C r :=
  by
  rw [isUnit_iff_totalDegree_of_isReduced, totalDegree_eq_zero_iff_eq_C]
  refine ⟨fun H ↦ ⟨_, H⟩, ?_⟩
  rintro ⟨r, hr, rfl⟩
  simpa

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