English
A detailed coefficient relation: the coefficient of n.some in the coefficient of optionEquivLeft f at n.none equals the coefficient of n in f.
Русский
Подробное соотношение коэффициентов: коэффициент n.some в коэффициенте optionEquivLeft f на n.none равен коэффициенту n в f.
LaTeX
$$$\mathrm{coeff}_{n}.\mathrm{some} (\mathrm{Polynomial}.\mathrm{coeff} (\mathrm{optionEquivLeft}\, f) (n.\mathrm{none})) = \mathrm{coeff}_n f$$$
Lean4
/-- The coefficient of `n.some` in the `n none`-th coefficient of `optionEquivLeft R S₁ f`
equals the coefficient of `n` in `f` -/
theorem optionEquivLeft_coeff_coeff (n : Option S₁ →₀ ℕ) (f : MvPolynomial (Option S₁) R) :
coeff n.some (Polynomial.coeff (optionEquivLeft R S₁ f) (n none)) = coeff n f := by
induction f using MvPolynomial.induction_on' generalizing n with
| monomial j r =>
rw [optionEquivLeft_monomial]
classical
simp only [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial, apply_ite]
simp only [coeff_zero]
by_cases hj : j = n
· simp [hj]
· rw [if_neg hj]
simp only [ite_eq_right_iff]
intro hj_none hj_some
apply False.elim (hj _)
simp only [Finsupp.ext_iff, Option.forall, hj_none, true_and]
simpa only [Finsupp.ext_iff] using hj_some
| add p q hp hq => simp only [map_add, Polynomial.coeff_add, coeff_add, hp, hq]
