leadingCoeff_add_eq_right — Mathlib

English

If y.orderTop < x.orderTop, then the leading coefficient of x+y equals the leading coefficient of y.

Русский

Если y.orderTop < x.orderTop, то ведущий коэффициент x+y равен ведущему коэффициенту y.

LaTeX

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

Lean4

theorem leadingCoeff_add_eq_right {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : y.orderTop < x.orderTop) :
    (x + y).leadingCoeff = y.leadingCoeff := by
  simpa [← map_add, ← AddOpposite.op_add, hxy] using
    leadingCoeff_add_eq_left (x := addOppositeEquiv.symm (.op y)) (y := addOppositeEquiv.symm (.op x))

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