teichmuller_coeff_zero

Mathlib.RingTheory.WittVector.Teichmuller

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

English

The 0-th coefficient of teichmuller p r equals r.

Русский

0-я компонента Teichmüller-поднятия равна r.

LaTeX

$$$(\\mathrm{teichmuller}\\ p \\ r).\\mathrm{coeff} 0 = r$$$

Lean4

@[simp]
theorem teichmuller_coeff_zero (r : R) : (teichmuller p r).coeff 0 = r :=
  rfl

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

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

Разделы

Аффилиация

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