map_polynomial — Mathlib

English

Under a base change by a ring homomorphism f, the polynomial defining the projective curve maps compatibly to the base-changed curve.

Русский

При базовом изменении кривая определяется полиномом, который отображается совместимо через соответствующее гомоморфизм баз.

LaTeX

$$$(W'.map f).polynomial = MvPolynomial.map f\, W'.polynomial$$$

Lean4

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

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