degree_pow' — Mathlib

English

For any n, deg(p^n) = n · deg(p) provided lc(p)^n ≠ 0.

Русский

Для любого n deg(p^n) = n · deg(p), если lc(p)^n ≠ 0.

LaTeX

$$deg(p^n) = n \cdot deg(p) при leadingCoeff(p)^n ≠ 0$$

Lean4

theorem degree_pow' : ∀ {n : ℕ}, leadingCoeff p ^ n ≠ 0 → degree (p ^ n) = n • degree p
  | 0 => fun h => by rw [pow_zero, ← C_1] at *; rw [degree_C h, zero_nsmul]
  | n + 1 => fun h =>
    by
    have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]
    have h₂ : leadingCoeff (p ^ n) * leadingCoeff p ≠ 0 := by rwa [pow_succ, ← leadingCoeff_pow' h₁] at h
    rw [pow_succ, degree_mul' h₂, succ_nsmul, degree_pow' h₁]

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