leadingCoeff_monomial — Mathlib

English

LeadingCoeff of a monomial equals its coefficient, by definition.

Русский

Старший коэффициент монома равен его коэффициенту по определению.

LaTeX

$$$m.leadingCoeff(LinearMap.instFunLike.coe( MvPolynomial.monomial d) c) = c$$$

Lean4

@[simp]
theorem leadingCoeff_monomial {d : σ →₀ ℕ} (c : R) : m.leadingCoeff (monomial d c) = c := by
  classical
  simp only [leadingCoeff, degree_monomial]
  split_ifs with hc <;> simp [hc]

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