baseChange_preΨ' — Mathlib

English

For the family of polynomials preΨ' parameterized by n, the base-changed preΨ' at B is the image under f of the base-changed preΨ' at A.

Русский

Для семейства полиномов preΨ' зависимого параметра n применимое к базовому изменению над B является изображением базового изменения над A через f.

LaTeX

$$$ (W.baseChange\ B).pre\\Psi'(n) = ((W.baseChange\ A).pre\\Psi'(n)).map f $$$

Lean4

theorem baseChange_preΨ' (n : ℕ) : (W.baseChange B).preΨ' n = ((W.baseChange A).preΨ' n).map f := by
  rw [← map_preΨ', map_baseChange]

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