totalDegree_monomial_le — Mathlib

English

The total degree of a monomial with coefficient c is bounded above by the sum of its exponents.

Русский

Общая степень мономиала с коэффициентом c ограничена суммой его степеней.

LaTeX

$$$\operatorname{totalDegree}(\operatorname{monomial}(s) \; c) \le \sum_i s(i)$$$

Lean4

theorem totalDegree_monomial_le (s : σ →₀ ℕ) (c : R) : (monomial s c).totalDegree ≤ s.sum fun _ ↦ id := by
  if hc : c = 0 then simp only [hc, map_zero, totalDegree_zero, zero_le]
  else rw [totalDegree_monomial _ hc, Function.id_def]

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