leadingCoeff_one

Mathlib.RingTheory.HahnSeries.Multiplication

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

English

The leading coefficient of the unit Hahn series 1 is 1.

Русский

Ведущий коэффициент единичной ГансСерии равен 1.

LaTeX

$$$\mathrm{leadingCoeff}(1) = 1$$$

Lean4

@[simp]
theorem leadingCoeff_one [MulZeroOneClass R] : (1 : HahnSeries Γ R).leadingCoeff = 1 := by simp [leadingCoeff_eq]

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

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

Разделы

Аффилиация

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