case inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : DecidableEq R
i : ℕ
r : R
hr : r = 0
⊢ natDegree (↑(monomial i) r) = 0

case inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : DecidableEq R
i : ℕ
r : R
hr : ¬r = 0
⊢ natDegree (↑(monomial i) r) = i
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : DecidableEq R
i : ℕ
r : R
⊢ natDegree (↑(monomial i) r) = if r = 0 then 0 else i
split_ifs with hr
no goals
case inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : DecidableEq R
i : ℕ
r : R
hr : r = 0
⊢ natDegree (↑(monomial i) r) = 0
simp [hr]
no goals
case inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : DecidableEq R
i : ℕ
r : R
hr : ¬r = 0
⊢ natDegree (↑(monomial i) r) = i
rw [← C_mul_X_pow_eq_monomial, natDegree_C_mul_X_pow i r hr]