natDegree_pow — Mathlib

English

If p is monic, then natDegree(p^n) = n · natDegree(p).

Русский

Если p моноическое, то natDegree(p^n) = n · natDegree(p).

LaTeX

$$$Monic(p) \Rightarrow \forall n \in \mathbb{N}, \; \operatorname{natDegree}(p^n) = n \cdot \operatorname{natDegree}(p)$$$

Lean4

theorem natDegree_pow (hp : p.Monic) (n : ℕ) : (p ^ n).natDegree = n * p.natDegree := by
  induction n with
  | zero => simp
  | succ n hn => rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]

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