degreeOf_monomial_eq — Mathlib

English

For a monomial m with nonzero coefficient a, degreeOf i (monomial m) equals m(i).

Русский

Для монома m с ненулевым коэффициентом степень degreeOf i(monomial m) равна m(i).

LaTeX

$$$\deg_i(\mathrm{monomial}\, s) = s(i)$, при $a \neq 0$$$

Lean4

theorem degreeOf_monomial_eq (s : σ →₀ ℕ) (i : σ) {a : R} (ha : a ≠ 0) : (monomial s a).degreeOf i = s i := by
  classical
    rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]
    -- TODO we can prove equality with `NoZeroDivisors R`

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