degree_eq_one_of_irreducible_of_root

English

If p is irreducible and Has a root x, then deg p = 1.

Русский

Если p ир Reducible и имеет корень x, то deg p = 1.

LaTeX

$$$ \text{Irreducible}(p) \; \Rightarrow\; \deg p = 1 \text{ if } p(x)=0 $$$

Lean4

theorem degree_eq_one_of_irreducible_of_root (hi : Irreducible p) {x : R} (hx : IsRoot p x) : degree p = 1 :=
  let ⟨g, hg⟩ := dvd_iff_isRoot.2 hx
  have : IsUnit (X - C x) ∨ IsUnit g := hi.isUnit_or_isUnit hg
  this.elim
    (fun h => by
      have h₁ : degree (X - C x) = 1 := degree_X_sub_C x
      have h₂ : degree (X - C x) = 0 := degree_eq_zero_of_isUnit h
      rw [h₁] at h₂; exact absurd h₂ (by decide))
    fun hgu => by rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]

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