English
On a monomial m, optionEquivLeft maps to a product of two monomials, one indexed by none and one by some, in the target polynomial ring.
Русский
На мономе m отображение optionEquivLeft превращает его в произведение двух мономов, индексируемых none и some, в целевом полиноме.
LaTeX
$$$\text{optionEquivLeft}(\text{monomial } m\ r) = \text{monomial}(m\text{ none})\;\text{(monomial } m.some\; r)$$$
Lean4
theorem optionEquivLeft_monomial (m : Option S₁ →₀ ℕ) (r : R) :
optionEquivLeft R S₁ (monomial m r) = .monomial (m none) (monomial m.some r) :=
by
rw [optionEquivLeft_apply, aeval_monomial, prod_option_index]
· rw [MvPolynomial.monomial_eq, ← Polynomial.C_mul_X_pow_eq_monomial]
simp only [Polynomial.algebraMap_apply, algebraMap_eq, Option.elim_none, Option.elim_some, map_mul, mul_assoc]
simp only [mul_comm, map_finsuppProd, map_pow]
· simp
· intros; rw [pow_add]
