natDegree_pow_X_add_C — Mathlib

English

For a nontrivial ring, natDegree((X + C r)^n) = n for all n and r.

Русский

Для ненулевого кольца natDegree((X + C r)^n) = n для всех n и r.

LaTeX

$$$[\text{Nontrivial}(R)] \Rightarrow \forall n \in \mathbb{N}, \forall r \in R, \; \operatorname{natDegree}((X + C r)^n) = n$$$

Lean4

@[simp]
theorem natDegree_pow_X_add_C [Nontrivial R] (n : ℕ) (r : R) : ((X + C r) ^ n).natDegree = n := by
  rw [(monic_X_add_C r).natDegree_pow, natDegree_X_add_C, mul_one]

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