trinomial_leadingCoeff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem trinomial_leadingCoeff (hkm : k < m) (hmn : m < n) (hw : w ≠ 0) : (trinomial k m n u v w).leadingCoeff = w := by
  rw [leadingCoeff, trinomial_natDegree hkm hmn hw, trinomial_leading_coeff' hkm hmn]

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