coeff_zero_right

Mathlib.SetTheory.Ordinal.CantorNormalForm

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

English

For any b, the coefficient function with o = 0 is identically zero: coeff(b,0) = 0.

Русский

Для любого b функция коэффициентов при o = 0 равна нулю: coeff(b,0) = 0.

LaTeX

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

Lean4

@[simp]
theorem coeff_zero_right (b : Ordinal) : coeff b 0 = 0 :=
  by
  ext e
  exact coeff_zero_apply b e

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

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

Разделы

Аффилиация

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