ghostComponent_verschiebung — Mathlib

English

The ghost component at index n+1 of Verschiebung equals p times the ghost component at index n of the original Witt vector.

Русский

Г ghost-компонента на позиции n+1 для Verschiebung равна p умноженному на ghost-компоненту на позиции n исходного Witt-вектора.

LaTeX

$$$$ ghostComponent_{n+1}(\\\\text{verschiebung}(x)) = p \\cdot ghostComponent_n(x). $$$$

Lean4

@[ghost_simps]
theorem ghostComponent_verschiebung (x : 𝕎 R) (n : ℕ) :
    ghostComponent (n + 1) (verschiebung x) = p * ghostComponent n x :=
  ghostComponent_verschiebungFun _ _

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