map_addX — Mathlib

English

Base-changing a Weierstrass affine curve commutes with the addition polynomial: the base-changed addition polynomial equals the image of the original under the base-change map.

Русский

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

LaTeX

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

Lean4

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

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