English
If coefficient nonzero, degreeOf in monomial equals its exponent vector entry.
Русский
Если коэффициент ненулевой, deg в мономе равен соответствующей компоненте экспоненты.
LaTeX
$$$\deg_i(\mathrm{monomial}\, s) = s(i)$ при ненулевом коэффициенте$$
Lean4
theorem totalDegree_add_eq_left_of_totalDegree_lt {p q : MvPolynomial σ R} (h : q.totalDegree < p.totalDegree) :
(p + q).totalDegree = p.totalDegree := by
classical
apply le_antisymm
· rw [← max_eq_left_of_lt h]
exact totalDegree_add p q
by_cases hp : p = 0
· simp [hp]
obtain ⟨b, hb₁, hb₂⟩ :=
p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ => Multiset.card (toMultiset m)
have hb : b ∉ q.support := by
contrapose! h
rw [totalDegree_eq p, hb₂, totalDegree_eq]
apply Finset.le_sup h
have hbb : b ∈ (p + q).support := by
apply support_sdiff_support_subset_support_add
rw [Finset.mem_sdiff]
exact ⟨hb₁, hb⟩
rw [totalDegree_eq, hb₂, totalDegree_eq]
exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
