pow — Mathlib

English

If p is monic of degree m, then p^n is monic of degree m·n.

Русский

Если p монический степеня m, то p^n монический и имеет степень m·n.

LaTeX

$$$ (p^{n}) \text{ is monic of degree } (m \cdot n)$$$

Lean4

theorem pow {p : R[X]} {m : ℕ} (hp : IsMonicOfDegree p m) (n : ℕ) : IsMonicOfDegree (p ^ n) (m * n) := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, mul_add, mul_one]
    exact ih.mul hp

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