le_trailingDegree_monomial — Mathlib

English

For any R and any a, n, the trailing-degree of the monomial a X^n is at least n. Equivalently, trailingDegree(monomial n a) ≥ n.

Русский

Для любых R и любых a, n трайлDegree мономиала a X^n не меньше n; то есть trailingDegree(monomial n a) ≥ n.

LaTeX

$$$\operatorname{trailingDegree}(\mathrm{monomial}(n, a)) \ge n$$$

Lean4

theorem le_trailingDegree_monomial : ↑n ≤ trailingDegree (monomial n a) :=
  letI := Classical.decEq R
  if ha : a = 0 then by simp [ha] else (trailingDegree_monomial ha).ge

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