verschiebungFun_coeff_zero

Mathlib.RingTheory.WittVector.Verschiebung

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

English

The 0th coefficient of verschiebungFun x is 0 for any Witt vector x.

Русский

Нулевой коэффициент verschiebungFun x равен 0 для любого Witt-вектора x.

LaTeX

$$$$ (\\\\text{verschiebungFun}(x))_0 = 0. $$$$

Lean4

theorem verschiebungFun_coeff_zero (x : 𝕎 R) : (verschiebungFun x).coeff 0 = 0 := by
  rw [verschiebungFun_coeff, if_pos rfl]

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

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

Разделы

Аффилиация

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