R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hpq : ¬Monic q
⊢ ¬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
hpq : Monic (p * q)
⊢ Monic q
contrapose! hpq
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hpq : ¬Polynomial.leadingCoeff q = 1
⊢ ¬Polynomial.leadingCoeff (p * q) = 1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hpq : ¬Monic q
⊢ ¬Monic (p * q)
rw [Monic.def] at hpq⊢
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
hpq : ¬Polynomial.leadingCoeff q = 1
⊢ ¬Polynomial.leadingCoeff (p * q) = 1
rwa [leadingCoeff_monic_mul hp]