map_polynomialX — Mathlib

English

The X-polynomial of the mapped curve is the X-polynomial of the original curve composed with the coefficient map f.

Русский

Полином X-поля кривой после отображения равен полиному X исходной кривой, составленному с отображением коэффициентов f.

LaTeX

$$$(W.map f).toAffine.polynomialX = W.polynomialX.map (mapRingHom f)$$$

Lean4

theorem map_polynomialX : (W.map f).toAffine.polynomialX = W.polynomialX.map (mapRingHom f) :=
  by
  simp only [polynomialX]
  map_simp

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