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]
⊢ p * q = 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 → p * q = 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]
⊢ p * q = 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 : p * q = 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]
⊢ p * q = 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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 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 : p * q = 0
⊢ q = 0
rw [← smul_eq_zero_iff_eq h.unit⁻¹] at 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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
this : (IsUnit.unit h)⁻¹ • (p * q) = (IsUnit.unit h)⁻¹ • p * q
⊢ 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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
⊢ q = 0
have : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q := by
  ext
  simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
  refine' sum_congr rfl fun x _ => _
  rw [← mul_assoc]
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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • p * q = 0
this : (IsUnit.unit h)⁻¹ • (p * q) = (IsUnit.unit h)⁻¹ • p * q
⊢ Monic ((IsUnit.unit h)⁻¹ • p)
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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
this : (IsUnit.unit h)⁻¹ • (p * q) = (IsUnit.unit h)⁻¹ • p * q
⊢ q = 0
rwa [this, Monic.mul_right_eq_zero_iff] at hp
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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • p * q = 0
this : (IsUnit.unit h)⁻¹ • (p * q) = (IsUnit.unit h)⁻¹ • p * q
⊢ Monic ((IsUnit.unit h)⁻¹ • p)
exact monic_of_isUnit_leadingCoeff_inv_smul _
case a
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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ coeff ((IsUnit.unit h)⁻¹ • (p * q)) n✝ = coeff ((IsUnit.unit h)⁻¹ • p * q) n✝
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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
⊢ (IsUnit.unit h)⁻¹ • (p * q) = (IsUnit.unit h)⁻¹ • p * q
ext
case a
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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ ∑ x in Nat.antidiagonal n✝, ↑(IsUnit.unit h)⁻¹ * (coeff p x.fst * coeff q x.snd) =
    ∑ x in Nat.antidiagonal n✝, ↑(IsUnit.unit h)⁻¹ * coeff p x.fst * coeff q x.snd
case a
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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ coeff ((IsUnit.unit h)⁻¹ • (p * q)) n✝ = coeff ((IsUnit.unit h)⁻¹ • p * q) n✝
simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
case a
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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
n✝ : ℕ
x : ℕ × ℕ
x✝ : x ∈ Nat.antidiagonal n✝
⊢ ↑(IsUnit.unit h)⁻¹ * (coeff p x.fst * coeff q x.snd) = ↑(IsUnit.unit h)⁻¹ * coeff p x.fst * coeff q x.snd
case a
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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ ∑ x in Nat.antidiagonal n✝, ↑(IsUnit.unit h)⁻¹ * (coeff p x.fst * coeff q x.snd) =
    ∑ x in Nat.antidiagonal n✝, ↑(IsUnit.unit h)⁻¹ * coeff p x.fst * coeff q x.snd
refine' sum_congr rfl fun x _ => _
no goals
case a
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✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
n✝ : ℕ
x : ℕ × ℕ
x✝ : x ∈ Nat.antidiagonal n✝
⊢ ↑(IsUnit.unit h)⁻¹ * (coeff p x.fst * coeff q x.snd) = ↑(IsUnit.unit h)⁻¹ * coeff p x.fst * coeff q x.snd
rw [← mul_assoc]
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)
⊢ p * 0 = 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 → p * q = 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)
⊢ p * 0 = 0
simp