trailingDegree_C_mul_X_pow — Mathlib

English

If a ≠ 0, trailingDegree(C a · X^n) = n; i.e., multiplying a nonzero constant by X^n shifts the trailing-degree by n.

Русский

Если a ≠ 0, трайлDegree(C a · X^n) = n; умножение ненулевой константы на X^n смещает трайлDegree на n.

LaTeX

$$$a \neq 0 \Rightarrow \operatorname{trailingDegree}(C a \cdot X^{n}) = n$$$

Lean4

@[simp]
theorem trailingDegree_C_mul_X_pow (n : ℕ) (ha : a ≠ 0) : trailingDegree (C a * X ^ n) = n := by
  rw [C_mul_X_pow_eq_monomial, trailingDegree_monomial ha]

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