R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ↑(natTrailingDegree p) = ↑n ↔ natTrailingDegree p = n
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hp : p ≠ 0
⊢ trailingDegree p = ↑n ↔ natTrailingDegree p = n
rw [trailingDegree_eq_natTrailingDegree hp]
no goals
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ↑(natTrailingDegree p) = ↑n ↔ natTrailingDegree p = n
exact WithTop.coe_eq_coe