English
If p ≠ 0, then the non-bottom weighted total degree of p agrees with the ordinary weighted total degree when viewed in the ambient ordered structure, i.e., the WithBot value of the degree is the lifting of the degree in M.
Русский
Если p ≠ 0, то взвешенная суммарная степень p в режиме WithBot совпадает с обычной взвешенной суммой степеней, полученной в M (включение в WithBot).
LaTeX
$$$\\text{weightedTotalDegree}'(w,p) \\\\ = \\\\ ↑(\\text{weightedTotalDegree}(w,p))\\quad\\text{при } p \\neq 0$$$
Lean4
/-- This lemma relates `weightedTotalDegree` and `weightedTotalDegree'`. -/
theorem weightedTotalDegree_coe (w : σ → M) (p : MvPolynomial σ R) (hp : p ≠ 0) :
weightedTotalDegree' w p = ↑(weightedTotalDegree w p) :=
by
rw [Ne, ← weightedTotalDegree'_eq_bot_iff w p, ← Ne, WithBot.ne_bot_iff_exists] at hp
obtain ⟨m, hm⟩ := hp
apply le_antisymm
· simp only [weightedTotalDegree, weightedTotalDegree', Finset.sup_le_iff, WithBot.coe_le_coe]
intro b
exact Finset.le_sup
· simp only [weightedTotalDegree]
have hm' : weightedTotalDegree' w p ≤ m := le_of_eq hm.symm
rw [← hm]
simpa [weightedTotalDegree'] using hm'
