map_negPolynomial — Mathlib

English

Under a ring hom f, the negPolynomial commutes with the map of W' and its base polynomial, i.e., map of negPolynomial equals negPolynomial of mapped curve.

Русский

При отображении по кольскому гомоморфизму f полином neg согласуется с отображением кривой: map(negPolynomial) = negPolynomial(map).

LaTeX

$$$ (W'.map f).toAffine.negPolynomial = W'.negPolynomial.map (mapRingHom f) $$$

Lean4

theorem map_negPolynomial : (W'.map f).toAffine.negPolynomial = W'.negPolynomial.map (mapRingHom f) :=
  by
  simp only [negPolynomial]
  map_simp

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