no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.692387
p q : R[X]
hq : Monic q
H : leadingCoeff p = 0
⊢ leadingCoeff (p * q) = leadingCoeff p
rw [H, leadingCoeff_eq_zero.1 H, zero_mul, leadingCoeff_zero]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.692387
p q : R[X]
hq : Monic q
H : leadingCoeff p ≠ 0
⊢ leadingCoeff p * leadingCoeff q ≠ 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.692387
p q : R[X]
hq : Monic q
H : leadingCoeff p ≠ 0
⊢ leadingCoeff (p * q) = leadingCoeff p
rw [leadingCoeff_mul', hq.leadingCoeff, mul_one]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.692387
p q : R[X]
hq : Monic q
H : leadingCoeff p ≠ 0
⊢ leadingCoeff p * leadingCoeff q ≠ 0
rwa [hq.leadingCoeff, mul_one]