R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : 0 < p
h : Monic f
⊢ (if p ∣ natDegree f * p then coeff f (natDegree f * p / p) else 0) = 1
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : 0 < p
h : Monic f
⊢ Monic (↑(Polynomial.expand R p) f)
rw [Monic.def, Polynomial.leadingCoeff, natDegree_expand, coeff_expand hp]
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : 0 < p
h : Monic f
⊢ (if p ∣ natDegree f * p then coeff f (natDegree f * p / p) else 0) = 1
simp [hp, h]