natDegree_eq_zero_iff_eq_one — Mathlib

English

If p is monic, then natDegree p = 0 if and only if p = 1.

Русский

Если p моничен, то natDegree p = 0 тогда и только тогда, когда p = 1.

LaTeX

$$$\text{If } p\text{ is Monic, then } p.natDegree = 0 \iff p = 1.$$$

Lean4

@[simp]
theorem natDegree_eq_zero_iff_eq_one (hp : p.Monic) : p.natDegree = 0 ↔ p = 1 :=
  by
  constructor <;> intro h
  swap
  · rw [h]
    exact natDegree_one
  have : p = C (p.coeff 0) := by
    rw [← Polynomial.degree_le_zero_iff]
    rwa [Polynomial.natDegree_eq_zero_iff_degree_le_zero] at h
  rw [this]
  rw [← h, ← Polynomial.leadingCoeff, Monic.def.1 hp, C_1]

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