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