baseChange_polynomial — Mathlib

English

The polynomial of the base-changed Jacobian equals the image under f of the original polynomial.

Русский

Полином якобиана после изменения основания равен образу оригинального полинома через f.

LaTeX

$$$$ (W'.\\mathrm{baseChange} B).\\mathrm{toJacobian}.\\mathrm{polynomial} = \\mathrm{MvPolynomial.map}\, f\\, (W'.\\mathrm{baseChange} A).\\mathrm{toJacobian}.\\mathrm{polynomial} $$$$

Lean4

theorem baseChange_polynomial :
    (W'.baseChange B).toJacobian.polynomial = MvPolynomial.map f (W'.baseChange A).toJacobian.polynomial := by
  rw [← map_polynomial, map_baseChange]

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