trinomial_trailingCoeff — Mathlib

English

Let k < m < n and u ≠ 0. Then the trailing coefficient of the trinomial with parameters k, m, n and coefficients u, v, w is u.

Русский

Пусть k < m < n и u ≠ 0. Тогда хвостовой коэффициент trinomial(k, m, n, u, v, w) равен u.

LaTeX

$$$\\operatorname{trailingCoeff}\\left(\\operatorname{trinomial}(k,m,n,u,v,w)\\right) = u$$$

Lean4

theorem trinomial_trailingCoeff (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) : (trinomial k m n u v w).trailingCoeff = u :=
  by rw [trailingCoeff, trinomial_natTrailingDegree hkm hmn hu, trinomial_trailing_coeff' hkm hmn]

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