English
If x.orderTop < y.orderTop, then the leading coefficient of x+y equals the leading coefficient of x.
Русский
Если x.orderTop < y.orderTop, то ведущий коэффициент x+y равен ведущему коэффициенту x.
LaTeX
$$$$ (x+y).leadingCoeff = x.leadingCoeff \quad \text{if } x.orderTop < y.orderTop. $$$$
Lean4
theorem leadingCoeff_add_eq_left {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : x.orderTop < y.orderTop) :
(x + y).leadingCoeff = x.leadingCoeff :=
by
have hx : x ≠ 0 := orderTop_ne_top.1 hxy.ne_top
have ho : (x + y).orderTop = x.orderTop := orderTop_add_eq_left hxy
by_cases h : x + y = 0
· rw [h, orderTop_zero] at ho
rw [h, orderTop_eq_top.mp ho.symm]
· simp_rw [leadingCoeff_of_ne_zero h, leadingCoeff_of_ne_zero hx, ho, coeff_add]
rw [coeff_eq_zero_of_lt_orderTop (x := y) (by simpa using hxy), add_zero]
