one_coeff_zero

Mathlib.RingTheory.WittVector.Defs

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

English

The Witt vector 1 has its zero-th coefficient equal to 1: (1 : 𝕎 R).coeff 0 = 1.

Русский

Witt-вектор единицы имеет нулевой коэффициент равным 1: (1 : 𝕎 R).coeff 0 = 1.

LaTeX

$$$$ (1 : \mathbb{W}_p(R)).\mathrm{coeff}(0) = 1. $$$$

Lean4

@[simp]
theorem one_coeff_zero : (1 : 𝕎 R).coeff 0 = 1 :=
  show (aeval _ (wittOne p 0) : R) = 1 by simp only [wittOne_zero_eq_one, map_one]

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

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

Разделы

Аффилиация

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