trailingDegree_C — Mathlib

English

If a ≠ 0, then trailingDegree(C a) = 0; the trailing degree of a nonzero constant is zero.

Русский

Если a ≠ 0, то трайлDegree константного полинома C a равен 0; трайлDegree ненулевой константы равен нулю.

LaTeX

$$$a \neq 0 \Rightarrow \operatorname{trailingDegree}(C a) = 0$$$

Lean4

@[simp]
theorem trailingDegree_C (ha : a ≠ 0) : trailingDegree (C a) = (0 : ℕ∞) :=
  trailingDegree_monomial ha

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