verschiebung_zmod

Mathlib.RingTheory.WittVector.Identities

URI: https://scilib.ai/kg/mathlib#WittVector.verschiebung_zmod

← MathLib Explorer

English

In Witt vectors over Z/pZ, Verschiebung equals multiplication by p.

Русский

В Witt-векторах над Z/pZ Verschiebung равна умножению на p.

LaTeX

$$$\text{verschiebung}(x) = x \cdot p$ for x ∈ 𝕎(Z/pZ)$$

Lean4

/-- Verschiebung is the same as multiplication by `p` on the ring of Witt vectors of `ZMod p`. -/
theorem verschiebung_zmod (x : 𝕎 (ZMod p)) : verschiebung x = x * p := by rw [← frobenius_verschiebung, frobenius_zmodp]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru