aevalAeval_swap — Mathlib

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)

Похожие утверждения