case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : p = 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q

case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : ¬p = 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
by_cases hp : p = 0
no goals
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : p = 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
simp only [hp, zero_mul, leadingCoeff_zero]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q

case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : ¬p = 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
by_cases hq : q = 0
no goals
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
simp only [hq, mul_zero, leadingCoeff_zero]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ leadingCoeff p * leadingCoeff q ≠ 0
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q
rw [leadingCoeff_mul']
no goals
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ leadingCoeff p * leadingCoeff q ≠ 0
exact mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)