R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ↑(natDegree p) = ↑n ↔ natDegree p = n
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hp : p ≠ 0
⊢ degree p = ↑n ↔ natDegree p = n
rw [degree_eq_natDegree hp]
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ↑(natDegree p) = ↑n ↔ natDegree p = n
exact WithBot.coe_eq_coe