aveal_eq_map_swap — Mathlib

English

If x ∈ A and p ∈ R[X][Y], evaluating p at x after replacing X with x via C x is the same as mapping swap p through aeval x; i.e., aeval (C x) p = mapAlgHom (aeval x) (swap p).

Русский

Если x ∈ A и p ∈ R[X][Y], то вычисление p при подстановке X в x эквивалентно отображению swap p через aeval x: aeval (C x) p = mapAlgHom (aeval x) (swap p).

LaTeX

$$$\\mathrm{aeval}(\\mathrm{C}\\;x)\\; p = \\mathrm{mapAlgHom}(\\mathrm{aeval}(x))\\Bigl(\\mathrm{swap}(p)\\Bigr).$$$

Lean4

theorem aveal_eq_map_swap (x : A) (p : R[X][Y]) : aeval (C x) p = mapAlgHom (aeval x) (swap 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, C_mul_X_pow_eq_monomial])

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