map_polynomial — Mathlib

English

For any Ring hom f, the polynomial defining the Jacobian after mapping equals the image under f of the original polynomial.

Русский

Для любого кольцевого гомоморфа f полином, задающий якобиан после отображения, равен образу под действием f исходного полинома.

LaTeX

$$$$\\text{polynomial}((W'.\\mathrm{map} f)\\!\\to\\!\\mathrm{Jacobian}) = \\mathrm{MvPolynomial.map}\, f\\,W'.\\mathrm{polynomial}$$$$

Lean4

@[simp]
theorem map_polynomial : (W'.map f).toJacobian.polynomial = MvPolynomial.map f W'.polynomial :=
  by
  simp only [polynomial]
  map_simp

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