baseChange_polynomialY — Mathlib

English

The X-polynomial under base change B equals the X-polynomial under base change A mapped via f.

Русский

Полином X после базового переноса по B равен полиному X после переноса по A, отображённому через f.

LaTeX

$$$(W.baseChange B).toAffine.polynomialX = (W.baseChange A).toAffine.polynomialX.map (mapRingHom f)$$$

Lean4

theorem baseChange_polynomialY :
    (W.baseChange B).toAffine.polynomialY = (W.baseChange A).toAffine.polynomialY.map (mapRingHom f) := by
  rw [← map_polynomialY, map_baseChange]

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