R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
n : ℕ
⊢ Monic (p * p ^ n)
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
n : ℕ
⊢ Monic (p ^ (n + 1))
rw [pow_succ]
no goals
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
n : ℕ
⊢ Monic (p * p ^ n)
exact hp.mul (Monic.pow hp n)