leadingCoeff_sub — Mathlib

English

If x.orderTop < y.orderTop, then (x−y).leadingCoeff = x.leadingCoeff.

Русский

Если x.orderTop < y.orderTop, то (x−y).leadingCoeff = x.leadingCoeff.

LaTeX

$$$$ (x - y).leadingCoeff = x.leadingCoeff \quad \text{if } x.orderTop < y.orderTop. $$$$

Lean4

theorem leadingCoeff_sub {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : x.orderTop < y.orderTop) :
    (x - y).leadingCoeff = x.leadingCoeff := by
  rw [sub_eq_add_neg]
  rw [← orderTop_neg (x := y)] at hxy
  exact leadingCoeff_add_eq_left hxy

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