truncateFun_natCast

Mathlib.RingTheory.WittVector.Truncated

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

English

For every natural number m, truncating the Witt vector corresponding to m yields m in the truncated Witt vector: truncateFun n (m : 𝕎 R) = m.

Русский

Пусть m ∈ ℕ. Тогда усечение виттовектора, соответствующего m, дает m: truncateFun n (m : 𝕎 R) = m.

LaTeX

$$$$\\operatorname{truncateFun}_n(m) = m.$$$$

Lean4

theorem truncateFun_natCast (m : ℕ) : truncateFun n (m : 𝕎 R) = m :=
  rfl

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

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

Разделы

Аффилиация

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