case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
⊢ q * p = 0 → q = 0

case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
⊢ q = 0 → q * p = 0
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
⊢ q * p = 0 ↔ q = 0
constructor
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : q * p = 0
⊢ q = 0
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
⊢ q * p = 0 → q = 0
intro hp
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : q * p * ↑C ↑(IsUnit.unit h)⁻¹ = 0
⊢ q = 0
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : (fun x => x * ↑C ↑(IsUnit.unit h)⁻¹) (q * p) = (fun x => x * ↑C ↑(IsUnit.unit h)⁻¹) 0
⊢ q = 0
simp only [zero_mul] at hp
case mp.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : q * (p * ↑C ↑(IsUnit.unit h)⁻¹) = 0
⊢ Monic (p * ↑C ↑(IsUnit.unit h)⁻¹)
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : q * p * ↑C ↑(IsUnit.unit h)⁻¹ = 0
⊢ q = 0
rwa [mul_assoc, Monic.mul_left_eq_zero_iff] at hp
case mp.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : q * (p * ↑C ↑(IsUnit.unit h)⁻¹) = 0
⊢ leadingCoeff p * ↑(IsUnit.unit h)⁻¹ = 1
case mp.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : q * (p * ↑C ↑(IsUnit.unit h)⁻¹) = 0
⊢ Monic (p * ↑C ↑(IsUnit.unit h)⁻¹)
refine' monic_mul_C_of_leadingCoeff_mul_eq_one _
no goals
case mp.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : q * (p * ↑C ↑(IsUnit.unit h)⁻¹) = 0
⊢ leadingCoeff p * ↑(IsUnit.unit h)⁻¹ = 1
simp [Units.mul_inv_eq_iff_eq_mul, IsUnit.unit_spec]
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
⊢ 0 * p = 0
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
⊢ q = 0 → q * p = 0
rintro rfl
no goals
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
⊢ 0 * p = 0
rw [zero_mul]