R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : IsUnit p
✝ : Nontrivial R
⊢ natDegree p = 0
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : IsUnit p
⊢ natDegree p = 0
nontriviality R
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q✝ : R[X]
h : IsUnit p
✝ : Nontrivial R
q : R[X]
hq : p * q = 1
⊢ natDegree p = 0
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : IsUnit p
✝ : Nontrivial R
⊢ natDegree p = 0
obtain ⟨q, hq⟩ := h.exists_right_inv
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q✝ : R[X]
h : IsUnit p
✝ : Nontrivial R
q : R[X]
hq : p * q = 1
this : natDegree (p * q) = natDegree p + natDegree q
⊢ natDegree p = 0
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q✝ : R[X]
h : IsUnit p
✝ : Nontrivial R
q : R[X]
hq : p * q = 1
⊢ natDegree p = 0
have := natDegree_mul (left_ne_zero_of_mul_eq_one hq) (right_ne_zero_of_mul_eq_one hq)
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q✝ : R[X]
h : IsUnit p
✝ : Nontrivial R
q : R[X]
hq : p * q = 1
this : natDegree p = 0 ∧ natDegree q = 0
⊢ natDegree p = 0
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q✝ : R[X]
h : IsUnit p
✝ : Nontrivial R
q : R[X]
hq : p * q = 1
this : natDegree (p * q) = natDegree p + natDegree q
⊢ natDegree p = 0
rw [hq, natDegree_one, eq_comm, add_eq_zero_iff] at this
no goals
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q✝ : R[X]
h : IsUnit p
✝ : Nontrivial R
q : R[X]
hq : p * q = 1
this : natDegree p = 0 ∧ natDegree q = 0
⊢ natDegree p = 0
exact this.1