totalDegree_zero_iff_isHomogeneous

English

A polynomial has total degree zero if and only if it is homogeneous of degree 0.

Русский

Полином имеет общую степень ноль тогда и только тогда, когда он однороден степени 0.

LaTeX

$$$p.totalDegree = 0 \\iff p.IsHomogeneous 0$$$

Lean4

theorem totalDegree_zero_iff_isHomogeneous {p : MvPolynomial σ R} : p.totalDegree = 0 ↔ IsHomogeneous p 0 := by
  rw [← weightedTotalDegree_one, ← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsHomogeneous]

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