R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
h0 : ¬0 = 1
this : Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
⊢ Monic (p * q)
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
h0 : ¬0 = 1
⊢ Monic (p * q)
have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
  simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]
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
hq : Monic q
h0 : ¬0 = 1
this : Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
⊢ Monic (p * q)
rw [Monic.def, leadingCoeff_mul' this, Monic.def.1 hp, Monic.def.1 hq, one_mul]
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
hq : Monic q
h0 : ¬0 = 1
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]