truncateFun_intCast

Mathlib.RingTheory.WittVector.Truncated

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

English

For every integer m, truncating the Witt vector corresponding to m equals 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_intCast (m : ℤ) : truncateFun n (m : 𝕎 R) = m :=
  rfl

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

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

Разделы

Аффилиация

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