map_polynomialY — Mathlib

English

Similarly, the Y-polynomial commutes with mapping via f.

Русский

Аналогично: Y-полином сохраняет отображение через f.

LaTeX

$$$$ (W'.\\mathrm{map} f).\\mathrm{toJacobian}.\\mathrm{polynomialY} = \\mathrm{MvPolynomial.map}\, f\\, W'.\\mathrm{polynomialY} $$$$

Lean4

@[simp]
theorem map_polynomialY : (W'.map f).toJacobian.polynomialY = MvPolynomial.map f W'.polynomialY := by
  simp only [polynomialY, map_polynomial, pderiv_map]

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