leadingCoeff_pow' — Mathlib

English

If natDegree(p) ≤ n and p.coeff n = 1, then p is Monic.

Русский

Если natDegree(p) ≤ n и коэффициент при x^n равен 1, то p монична.

LaTeX

$$(natDegree p) ≤ n ∧ p.coeff n = 1 ⇒ p.Monic$$

Lean4

theorem leadingCoeff_pow' : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n :=
  Nat.recOn n (by simp) fun n ih h =>
    by
    have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]
    have h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0 := by rwa [pow_succ', ← ih h₁] at h
    rw [pow_succ', pow_succ', leadingCoeff_mul' h₂, ih h₁]

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