baseChange_polynomialZ — Mathlib

English

As above for the Z-coordinate. The Z-coordinate polynomial behaves compatibly with the base-change map under W'.baseChange B and W'.baseChange A.

Русский

Аналогично для Z-координаты: Z-полином кривой ведёт себя совместимо с отображением при базовом изменении.

LaTeX

$$$ (W'.baseChange B).toProjective.polynomialZ = \\mathrm{MvPolynomial.map}\\ f\\left((W'.baseChange A).toProjective.polynomialZ\\right) $$$

Lean4

theorem baseChange_polynomialZ :
    (W'.baseChange B).toProjective.polynomialZ = MvPolynomial.map f (W'.baseChange A).toProjective.polynomialZ := by
  rw [← map_polynomialZ, map_baseChange]

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