R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
⊢ p = 1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hm : Monic p
hpu : IsUnit p
⊢ p = 1
nontriviality R
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
q : R[X]
h : p * q = 1
⊢ p = 1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
⊢ p = 1
obtain ⟨q, h⟩ := hpu.exists_right_inv
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : natDegree (p * q) = natDegree p + natDegree q
⊢ p = 1
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
q : R[X]
h : p * q = 1
⊢ p = 1
have := hm.natDegree_mul' (right_ne_zero_of_mul_eq_one h)
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : natDegree p = 0 ∧ natDegree q = 0
⊢ p = 1
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : natDegree (p * q) = natDegree p + natDegree q
⊢ p = 1
rw [h, natDegree_one, eq_comm, add_eq_zero_iff] at this
no goals
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : natDegree p = 0 ∧ natDegree q = 0
⊢ p = 1
exact hm.natDegree_eq_zero_iff_eq_one.mp this.1