trinomial_middle_coeff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem trinomial_middle_coeff (hkm : k < m) (hmn : m < n) : (trinomial k m n u v w).coeff m = v := 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.ne',
    if_pos rfl, if_neg hmn.ne, zero_add, add_zero]

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