map_addPolynomial — Mathlib

English

The polynomial for addition after applying a ring hom is the image under the hom of the original addition polynomial.

Русский

Полином сложения после применения гомоморфизма отображается как образ исходного полинома сложения.

LaTeX

$$$ (W'.map f).toAffine.addPolynomial (f x) (f y) (f \ell) = (W'.addPolynomial x y \ell).map f $$$

Lean4

theorem map_addPolynomial : (W'.map f).toAffine.addPolynomial (f x) (f y) (f ℓ) = (W'.addPolynomial x y ℓ).map f :=
  by
  rw [addPolynomial, map_polynomial, eval_map, linePolynomial, addPolynomial, ← coe_mapRingHom, ← eval₂_hom,
    linePolynomial]
  simp

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