ghostComponent_frobenius — Mathlib

English

Frobenius on Witt vectors preserves ghost components up to a shift: ghostComponent n (frobenius x) = ghostComponent (n+1) x.

Русский

Frobenius на Witt-векторах сохраняет Ghost-компоненты, сдвигая индекс на единицу: ghostComponent n (frobenius x) = ghostComponent (n+1) x.

LaTeX

$$$$\text{ghostComponent}_n(\operatorname{frobenius}(x)) = \text{ghostComponent}_{n+1}(x).$$$$

Lean4

@[ghost_simps]
theorem ghostComponent_frobenius (n : ℕ) (x : 𝕎 R) : ghostComponent n (frobenius x) = ghostComponent (n + 1) x :=
  ghostComponent_frobeniusFun _ _

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