coeff_zero_apply

Mathlib.SetTheory.Ordinal.CantorNormalForm

URI: https://scilib.ai/kg/mathlib#Ordinal.CNF.coeff_zero_apply

English

For any b and e, the coefficient at e in CNF(b, 0) is zero: coeff(b,0,e) = 0.

Русский

Для любых b и e коэффициент при e в CNF(b,0) равен 0.

LaTeX

$$$$ \\forall b,e:\\; \\operatorname{coeff}(b,0,e) = 0 $$$$

Lean4

theorem coeff_zero_apply (b e : Ordinal) : coeff b 0 e = 0 :=
  by
  apply coeff_of_not_mem_CNF
  simp

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

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

Разделы

Аффилиация

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