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 : a * ai = 1
⊢ natDegree p = natDegree (p * 1)
nth_rw 1 [← mul_one 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 : a * ai = 1
⊢ natDegree (p * 1) = natDegree (p * ↑C a * ↑C ai)
rw [← C_1, ← au, RingHom.map_mul, ← mul_assoc]