trinomial_trailing_coeff' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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