baseChange_polynomialX — Mathlib

English

Under base change, the Y-coordinate polynomial maps compatibly with the base-changed curve.

Русский

При изменении базы полином Y отображается согласованно.

LaTeX

$$$(W'.baseChange B).toProjective.polynomialY = MvPolynomial.map f (W'.baseChange A).toProjective.polynomialY$$$

Lean4

theorem baseChange_polynomialX :
    (W'.baseChange B).toProjective.polynomialX = MvPolynomial.map f (W'.baseChange A).toProjective.polynomialX := by
  rw [← map_polynomialX, map_baseChange]

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