eq_one_of_isUnit — Mathlib

English

If p is monic and a unit, then p = 1.

Русский

Если p моноическое и обратимо, то p = 1.

LaTeX

$$$Monic(p) \land IsUnit(p) \Rightarrow p = 1$$$

Lean4

theorem eq_one_of_isUnit (hm : Monic p) (hpu : IsUnit p) : p = 1 :=
  by
  nontriviality R
  obtain ⟨q, h⟩ := hpu.exists_right_inv
  have := hm.natDegree_mul' (right_ne_zero_of_mul_eq_one h)
  rw [h, natDegree_one, eq_comm, add_eq_zero] at this
  exact hm.natDegree_eq_zero_iff_eq_one.mp this.1

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