English
For any f in the multivariable polynomial ring over Option S1 with coefficients in R, the natural degree of the transformed polynomial optionEquivLeft(R,S1)(f) equals the degree of None in f.
Русский
Для любого f изкольного многочлена в переменных Option S1 над R, натуральная степень образа optionEquivLeft(R,S1)(f) равна степени None в f.
LaTeX
$$$\\operatorname{natDegree}(\\operatorname{optionEquivLeft} R S_1\\;f) = \\operatorname{degreeOf} \\bigl(\\text{None}\\;\\;f\\bigr)$$$
Lean4
@[simp]
theorem natDegree_optionEquivLeft (p : MvPolynomial (Option S₁) R) :
(optionEquivLeft R S₁ p).natDegree = p.degreeOf .none :=
by
apply le_antisymm
· rw [Polynomial.natDegree_le_iff_coeff_eq_zero]
intro N hN
ext σ
trans p.coeff (σ.embDomain .some + .single .none N)
· simpa using optionEquivLeft_coeff_coeff R S₁ (σ.embDomain .some + .single .none N) p
simp only [coeff_zero, ← notMem_support_iff]
intro H
simpa using (degreeOf_lt_iff ((zero_le _).trans_lt hN)).mp hN _ H
· rw [degreeOf_le_iff]
intro σ hσ
refine Polynomial.le_natDegree_of_ne_zero fun H ↦ ?_
have := optionEquivLeft_coeff_coeff R S₁ σ p
rw [H, coeff_zero, eq_comm, ← notMem_support_iff] at this
exact this hσ
