isUnit_iff_totalDegree_of_isReduced

English

Assuming R is reduced, P is a unit in MvPolynomial σ R if and only if P_0 is a unit and totalDegree of P is zero.

Русский

При условии, что R редуцировано, P единичен в MvPolynomial σ R тогда и только тогда, когда P_0 единица и общая степень P равна нулю.

LaTeX

$$$$ [\\operatorname{IsReduced}(R)] \\Rightarrow \\operatorname{IsUnit}(P) \\iff \\operatorname{IsUnit}(P_0) \\wedge \\operatorname{totalDegree}(P) = 0. $$$$

Lean4

theorem isUnit_iff_totalDegree_of_isReduced [IsReduced R] : IsUnit P ↔ IsUnit (P.coeff 0) ∧ P.totalDegree = 0 :=
  by
  convert isUnit_iff (P := P)
  rw [totalDegree_eq_zero_iff]
  simp [not_imp_comm (a := _ = (0 : R)), Finsupp.ext_iff]

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