leadingCoeff_of_single

Mathlib.RingTheory.HahnSeries.Basic

URI: https://scilib.ai/kg/mathlib#HahnSeries.leadingCoeff_of_single

English

The leading coefficient of the singleton at a with coefficient r is r.

Русский

Ведущий коэффициент Hahn-серии с единственным членом на $a$ имеет значение $r$.

LaTeX

$$$ \\operatorname{leadingCoeff}(\\mathrm{single}(a,r)) = r $$$

Lean4

@[simp]
theorem leadingCoeff_of_single {a : Γ} {r : R} : leadingCoeff (single a r) = r := by
  by_cases h : r = 0 <;> simp [leadingCoeff, h]

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

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

Разделы

Аффилиация

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