degree_eq_zero_iff_totalDegree_eq_zero

English

The degree of f is zero if and only if the total degree of f is zero.

Русский

Степень f равна нулю тогда и только тогда, когда общая степень f равна нулю.

LaTeX

$$$m.degree f = 0 \iff f.totalDegree = 0$$$

Lean4

theorem degree_eq_zero_iff_totalDegree_eq_zero {f : MvPolynomial σ R} : m.degree f = 0 ↔ f.totalDegree = 0 :=
  by
  rw [← m.toSyn.injective.eq_iff]
  rw [map_zero, ← m.bot_eq_zero, eq_bot_iff, m.bot_eq_zero, ← m.toSyn.map_zero]
  rw [degree_le_iff]
  rw [totalDegree_eq_zero_iff]
  apply forall_congr'
  intro d
  apply imp_congr (rfl.to_iff)
  rw [map_zero, ← m.bot_eq_zero, ← eq_bot_iff, m.bot_eq_zero]
  simp only [EmbeddingLike.map_eq_zero_iff]
  exact Finsupp.ext_iff

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