trinomial_leading_coeff' — Mathlib

English

If k < m and m < n, then the coefficient of X^n in trinomial k m n u v w is w.

Русский

При k < m < n коэффициент при X^n в триномии равен w.

LaTeX

$$$$ [X^n]\\operatorname{trinomial}(k,m,n,u,v,w) = w \\quad \\text{if } k < m \\text{ and } m < n. $$$$

Lean4

theorem trinomial_leading_coeff' (hkm : k < m) (hmn : m < n) : (trinomial k m n u v w).coeff n = w := by
  rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]

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