baseChange_ψ — Mathlib

English

The base-change compatibility also holds for the ψ polynomial without the integer-index: the base-changed ψ equals the image under f of the base-changed ψ.

Русский

Совместимость базового изменения сохраняется и для полинома ψ без индекса: ψ базового изменения равен образу ψ над A через f.

LaTeX

$$$ (W.baseChange\ B).\\psi(n) = ((W.baseChange\ A).\\psi(n)).map (mapRingHom f) $$$

Lean4

theorem baseChange_ψ (n : ℤ) : (W.baseChange B).ψ n = ((W.baseChange A).ψ n).map (mapRingHom f) := by
  rw [← map_ψ, map_baseChange]

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