map_negAddY — Mathlib

English

Similarly for the algebra-structured base change, the base-changed addition polynomial maps to the original via the algebra hom.

Русский

Аналогично в оснований базисной базы для алгебраического отображения: сложение полиномы сохраняют форму под отображением.

LaTeX

$$ (W'.baseChange B).toAffine.addPolynomial (f x) (f y) (f \ell) = ((W'.baseChange A).toAffine.addPolynomial x y ℓ).map f $$

Lean4

theorem map_negAddY : (W'.map f).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f ℓ) = f (W'.negAddY x₁ x₂ y₁ ℓ) :=
  by
  simp only [negAddY, map_addX]
  map_simp

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