R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ Option.getD (↑n) 0 = n
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ natTrailingDegree (↑(monomial n) a) = n
rw [natTrailingDegree, trailingDegree_monomial ha]
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ Option.getD (↑n) 0 = n
rfl