coeff_order_of_eq_add_single — Mathlib

English

If x = y + single x.order x.leadingCoeff, then the coefficient of y at x.order is zero.

Русский

Если x = y + единичный член в порядке x.order, то коэффициент y при x.order равен нулю.

LaTeX

$$$$ y .\text{coeff}(x.order) = 0 $$$$

Lean4

theorem coeff_order_of_eq_add_single {R} [AddCancelCommMonoid R] [Zero Γ] {x y : HahnSeries Γ R}
    (hxy : x = y + single x.order x.leadingCoeff) : y.coeff x.order = 0 := by
  simpa [← leadingCoeff_eq] using congr(($hxy).coeff x.order)

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