English
Evaluation preserves divisibility: if p divides q in the polynomial ring, then eval₂ f g(p) divides eval₂ f g(q).
Русский
Оценка сохраняет делимость: если p делит q в полиномном кольце, то eval₂ f g(p) делит eval₂ f g(q).
LaTeX
$$$\text{If } p \mid q,\; \; p.eval₂ f g \;|\; q.eval₂ f g$$$
Lean4
theorem eval₂_mul_monomial : ∀ {s a}, (p * monomial s a).eval₂ f g = p.eval₂ f g * f a * s.prod fun n e => g n ^ e := by
classical
apply MvPolynomial.induction_on p
· intro a' s a
simp [C_mul_monomial, eval₂_monomial, f.map_mul]
· intro p q ih_p ih_q
simp [add_mul, eval₂_add, ih_p, ih_q]
· intro p n ih s a
exact
calc
(p * X n * monomial s a).eval₂ f g
_ = (p * monomial (Finsupp.single n 1 + s) a).eval₂ f g := by rw [monomial_single_add, pow_one, mul_assoc]
_ = (p * monomial (Finsupp.single n 1) 1).eval₂ f g * f a * s.prod fun n e => g n ^ e := by
simp [ih, prod_single_index, prod_add_index, pow_one, pow_add, mul_assoc, mul_left_comm, f.map_one]
