English
Evaluating the swapped polynomial at (x,y) is the same as swapping and then evaluating at (y,x); i.e., aevalAeval x y (swap p) = aevalAeval y x p.
Русский
Оценка подстановки_SWAP p на (x,y) равна оценке p на (y,x): aevalAeval x y (swap p) = aevalAeval y x p.
LaTeX
$$$\\forall x,y:\\, aevalAeval\\ x\\ y\\ (swap\\ p) = aevalAeval\\ y\\ x\\ p.$$$
Lean4
/-- Evaluating `swap p` at `x`, `y` is the same as evaluating `p` at `y` `x`. -/
theorem aevalAeval_swap (x y : A) (p : R[X][Y]) : aevalAeval x y (swap p) = aevalAeval y x p := by
induction p using Polynomial.induction_on' with
| add => aesop
| monomial n a =>
simp
induction a using Polynomial.induction_on' <;> aesop (add norm add_mul)