English
For any p in MvPolynomial(Option S1) and i, the total degree of the i-th coefficient of optionEquivLeft(R,S1)(p) is at most p.totalDegree.
Русский
Для любого p ∈ MvPolynomial(Option S1) и любого i, totalDegree(coef_i(optionEquivLeft(R,S1)(p))) ≤ totalDegree(p).
LaTeX
$$$\\operatorname{totalDegree}(((\\operatorname{optionEquivLeft} R S_1\\;p).\\coeff i)).\\text{totalDegree} \\le p.totalDegree$$$
Lean4
theorem totalDegree_coeff_optionEquivLeft_le (p : MvPolynomial (Option S₁) R) (i : ℕ) :
((optionEquivLeft R S₁ p).coeff i).totalDegree ≤ p.totalDegree := by
classical
by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
· rw [hpi]; simp
rw [totalDegree, Finset.sup_le_iff]
intro σ hσ
refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
· simp [Finsupp.sum_add_index, Finsupp.sum_embDomain]
· simpa [mem_support_iff, ← optionEquivLeft_coeff_coeff R S₁] using hσ
