teichmuller_coeff_pos

Mathlib.RingTheory.WittVector.Teichmuller

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

English

All positive-index coefficients of teichmuller p r vanish: for n > 0, (teichmuller p r).coeff n = 0.

Русский

Все коэффициенты с положительным индексом равны нулю: если n > 0, то (teichmuller p r).coeff n = 0.

LaTeX

$$$\\forall n>0,\\; (teichmuller p r).coeff n = 0$$$

Lean4

@[simp]
theorem teichmuller_coeff_pos (r : R) : ∀ (n : ℕ) (_ : 0 < n), (teichmuller p r).coeff n = 0
  | _ + 1, _ => rfl

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

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

Разделы

Аффилиация

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