isMonicOfDegree_zero_iff — Mathlib

English

For any semiring R, a polynomial p ∈ R[X] is monic of degree 0 if and only if p = 1.

Русский

Для любого полугруппы R полином p ∈ R[X] мономичен ровно тогда, когда deg(p) = 0, то есть p = 1.

LaTeX

$$$$ IsMonicOfDegree(p, 0) \\iff p = 1. $$$$

Lean4

@[simp]
theorem isMonicOfDegree_zero_iff {p : R[X]} : IsMonicOfDegree p 0 ↔ p = 1 :=
  by
  simp only [isMonicOfDegree_iff']
  refine ⟨fun ⟨H₁, H₂⟩ ↦ eq_one_of_monic_natDegree_zero H₂ H₁, fun H ↦ ?_⟩
  subst H
  simp

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