coeff_mul_order_add_order — Mathlib

English

At the sum of orders, the coefficient equals the product of leading coefficients.

Русский

На сумме порядков коэффициент равен произведению ведущих коэффициентов.

LaTeX

$$$ (x*y)_{(x.order + y.order)} = x.leadingCoeff \cdot y.leadingCoeff $$$

Lean4

theorem coeff_mul_order_add_order (x y : HahnSeries Γ R) :
    (x * y).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff :=
  by
  simp only [← of_symm_smul_of_eq_mul]
  exact HahnModule.coeff_smul_order_add_order x y

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