coeff_add_monomial_mul — Mathlib

English

The coefficient at m + n of monomial m a ⋅ φ equals a ⋅ coeff n φ.

Русский

Коэффициент в m+n от мономиала m a ⋅ φ равен a ⋅ coeff n φ.

LaTeX

$$$$ \\operatorname{coeff}_{m+n}(\\operatorname{monomial}(m, a) \\cdot \\phi) = a \\cdot \\operatorname{coeff}_{n} \\phi $$$$

Lean4

theorem coeff_add_monomial_mul (a : R) : coeff (m + n) (monomial m a * φ) = a * coeff n φ :=
  by
  rw [coeff_monomial_mul, if_pos, add_tsub_cancel_left]
  exact le_add_right le_rfl

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