no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
ai : R
au : ai * a = 1
⊢ natDegree p = natDegree (1 * p)
nth_rw 1 [← one_mul p]
no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
ai : R
au : ai * a = 1
⊢ natDegree (1 * p) = natDegree (↑C ai * (↑C a * p))
rw [← C_1, ← au, RingHom.map_mul, ← mul_assoc]