[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
⊢ Subsingleton R → (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b
[PROOFSTEP]
intro
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
a✝ : Subsingleton R
⊢ (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ p = X ^ natDegree p + ∑ i in range (natDegree p), ↑C (coeff p i) * X ^ i
[PROOFSTEP]
conv_lhs => rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
| p
[PROOFSTEP]
rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
| p
[PROOFSTEP]
rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
| p
[PROOFSTEP]
rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ ↑C (coeff p (natDegree p)) * X ^ natDegree p + ∑ x in range (natDegree p), ↑C (coeff p x) * X ^ x =
    X ^ natDegree p + ∑ i in range (natDegree p), ↑C (coeff p i) * X ^ i
[PROOFSTEP]
suffices C (p.coeff p.natDegree) = 1 by rw [this, one_mul]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
this : ↑C (coeff p (natDegree p)) = 1
⊢ ↑C (coeff p (natDegree p)) * X ^ natDegree p + ∑ x in range (natDegree p), ↑C (coeff p x) * X ^ x =
    X ^ natDegree p + ∑ i in range (natDegree p), ↑C (coeff p i) * X ^ i
[PROOFSTEP]
rw [this, one_mul]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ ↑C (coeff p (natDegree p)) = 1
[PROOFSTEP]
exact congr_arg C hp
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
hq : Monic q
⊢ q ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r : R[X]
hp : p ≠ 0
hq : Monic 0
⊢ False
[PROOFSTEP]
rw [Monic.def, leadingCoeff_zero] at hq 
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r : R[X]
hp : p ≠ 0
hq : 0 = 1
⊢ False
[PROOFSTEP]
rw [← mul_one p, ← C_1, ← hq, C_0, mul_zero] at hp 
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r : R[X]
hp : 0 ≠ 0
hq : 0 = 1
⊢ False
[PROOFSTEP]
exact hp rfl
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
⊢ Monic (Polynomial.map f p)
[PROOFSTEP]
unfold Monic
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
⊢ Polynomial.leadingCoeff (Polynomial.map f p) = 1
[PROOFSTEP]
nontriviality
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
⊢ Polynomial.leadingCoeff (Polynomial.map f p) = 1
[PROOFSTEP]
have : f p.leadingCoeff ≠ 0 := by
  rw [show _ = _ from hp, f.map_one]
  exact one_ne_zero
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
⊢ ↑f (Polynomial.leadingCoeff p) ≠ 0
[PROOFSTEP]
rw [show _ = _ from hp, f.map_one]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
this : ↑f (Polynomial.leadingCoeff p) ≠ 0
⊢ Polynomial.leadingCoeff (Polynomial.map f p) = 1
[PROOFSTEP]
rw [Polynomial.leadingCoeff, coeff_map]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
this : ↑f (Polynomial.leadingCoeff p) ≠ 0
⊢ ↑f (coeff p (natDegree (Polynomial.map f p))) = 1
[PROOFSTEP]
suffices p.coeff (p.map f).natDegree = 1 by simp [this]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
this✝ : ↑f (Polynomial.leadingCoeff p) ≠ 0
this : coeff p (natDegree (Polynomial.map f p)) = 1
⊢ ↑f (coeff p (natDegree (Polynomial.map f p))) = 1
[PROOFSTEP]
simp [this]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
this : ↑f (Polynomial.leadingCoeff p) ≠ 0
⊢ coeff p (natDegree (Polynomial.map f p)) = 1
[PROOFSTEP]
rwa [natDegree_eq_of_degree_eq (degree_map_eq_of_leadingCoeff_ne_zero f this)]
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : b * leadingCoeff p = 1
⊢ Monic (↑C b * p)
[PROOFSTEP]
unfold Monic
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : b * leadingCoeff p = 1
⊢ leadingCoeff (↑C b * p) = 1
[PROOFSTEP]
nontriviality
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : b * leadingCoeff p = 1
✝ : Nontrivial R
⊢ leadingCoeff (↑C b * p) = 1
[PROOFSTEP]
rw [leadingCoeff_mul' _]
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : b * leadingCoeff p = 1
✝ : Nontrivial R
⊢ leadingCoeff (↑C b) * leadingCoeff p = 1
[PROOFSTEP]
simp [leadingCoeff_C b, hp]
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : b * leadingCoeff p = 1
✝ : Nontrivial R
⊢ leadingCoeff (↑C b) * leadingCoeff p ≠ 0
[PROOFSTEP]
simp [leadingCoeff_C b, hp]
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
⊢ Monic (p * ↑C b)
[PROOFSTEP]
unfold Monic
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
⊢ leadingCoeff (p * ↑C b) = 1
[PROOFSTEP]
nontriviality
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
✝ : Nontrivial R
⊢ leadingCoeff (p * ↑C b) = 1
[PROOFSTEP]
rw [leadingCoeff_mul' _]
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
✝ : Nontrivial R
⊢ leadingCoeff p * leadingCoeff (↑C b) = 1
[PROOFSTEP]
simp [leadingCoeff_C b, hp]
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
✝ : Nontrivial R
⊢ leadingCoeff p * leadingCoeff (↑C b) ≠ 0
[PROOFSTEP]
simp [leadingCoeff_C b, hp]
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
n : ℕ
H1 : degree p ≤ ↑n
H2 : coeff p n = 1
H : ¬degree p < ↑n
⊢ Monic p
[PROOFSTEP]
rwa [Monic, Polynomial.leadingCoeff, natDegree, (lt_or_eq_of_le H1).resolve_left H]
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
n : ℕ
H : degree p ≤ ↑n
H1 : degree p < ↑(n + 1)
⊢ coeff (X ^ (n + 1) + p) (n + 1) = 1
[PROOFSTEP]
rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H1, add_zero]
[GOAL]
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)
[PROOFSTEP]
have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]
[GOAL]
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
[PROOFSTEP]
simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]
[GOAL]
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)
[PROOFSTEP]
rw [Monic.def, leadingCoeff_mul' this, Monic.def.1 hp, Monic.def.1 hq, one_mul]
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
n : ℕ
⊢ Monic (p ^ (n + 1))
[PROOFSTEP]
rw [pow_succ]
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
n : ℕ
⊢ Monic (p * p ^ n)
[PROOFSTEP]
exact hp.mul (Monic.pow hp n)
[GOAL]
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 : degree q < degree p
⊢ Monic (p + q)
[PROOFSTEP]
rwa [Monic, add_comm, leadingCoeff_add_of_degree_lt hpq]
[GOAL]
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 : degree p < degree q
⊢ Monic (p + q)
[PROOFSTEP]
rwa [Monic, leadingCoeff_add_of_degree_lt hpq]
[GOAL]
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
[PROOFSTEP]
contrapose! hpq
[GOAL]
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)
[PROOFSTEP]
rw [Monic.def] at hpq ⊢
[GOAL]
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
[PROOFSTEP]
rwa [leadingCoeff_monic_mul hp]
[GOAL]
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
[PROOFSTEP]
contrapose! hpq
[GOAL]
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)
[PROOFSTEP]
rw [Monic.def] at hpq ⊢
[GOAL]
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
[PROOFSTEP]
rwa [leadingCoeff_mul_monic hq]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ natDegree p = 0 ↔ p = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ natDegree p = 0 → p = 1
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ p = 1 → natDegree p = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ p = 1
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : p = 1
⊢ natDegree p = 0
[PROOFSTEP]
swap
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : p = 1
⊢ natDegree p = 0
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : p = 1
⊢ natDegree 1 = 0
[PROOFSTEP]
exact natDegree_one
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ p = 1
[PROOFSTEP]
have : p = C (p.coeff 0) := by
  rw [← Polynomial.degree_le_zero_iff]
  rwa [Polynomial.natDegree_eq_zero_iff_degree_le_zero] at h 
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
rw [← Polynomial.degree_le_zero_iff]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ degree p ≤ 0
[PROOFSTEP]
rwa [Polynomial.natDegree_eq_zero_iff_degree_le_zero] at h 
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
this : p = ↑C (coeff p 0)
⊢ p = 1
[PROOFSTEP]
rw [this]
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
this : p = ↑C (coeff p 0)
⊢ ↑C (coeff p 0) = 1
[PROOFSTEP]
rw [← h, ← Polynomial.leadingCoeff, Monic.def.1 hp, C_1]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ degree p ≤ 0 ↔ p = 1
[PROOFSTEP]
rw [← hp.natDegree_eq_zero_iff_eq_one, natDegree_eq_zero_iff_degree_le_zero]
[GOAL]
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
⊢ natDegree (p * q) = natDegree p + natDegree q
[PROOFSTEP]
nontriviality R
[GOAL]
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
✝ : Nontrivial R
⊢ natDegree (p * q) = natDegree p + natDegree q
[PROOFSTEP]
apply natDegree_mul'
[GOAL]
case h
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
✝ : Nontrivial R
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
[PROOFSTEP]
simp [hp.leadingCoeff, hq.leadingCoeff]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
⊢ degree (p * q) = degree (q * p)
[PROOFSTEP]
by_cases h : q = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : q = 0
⊢ degree (p * q) = degree (q * p)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ degree (p * q) = degree (q * p)
[PROOFSTEP]
rw [degree_mul', hp.degree_mul]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ degree p + degree q = degree q + degree p
[PROOFSTEP]
exact add_comm _ _
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
[PROOFSTEP]
rwa [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]
[GOAL]
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 : q ≠ 0
⊢ natDegree (p * q) = natDegree p + natDegree q
[PROOFSTEP]
rw [natDegree_mul', add_comm]
[GOAL]
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 : q ≠ 0
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
[PROOFSTEP]
simpa [hp.leadingCoeff, leadingCoeff_ne_zero]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
⊢ natDegree (p * q) = natDegree (q * p)
[PROOFSTEP]
by_cases h : q = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : q = 0
⊢ natDegree (p * q) = natDegree (q * p)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ natDegree (p * q) = natDegree (q * p)
[PROOFSTEP]
rw [hp.natDegree_mul' h, Polynomial.natDegree_mul', add_comm]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ Polynomial.leadingCoeff q * Polynomial.leadingCoeff p ≠ 0
[PROOFSTEP]
simpa [hp.leadingCoeff, leadingCoeff_ne_zero]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h0 : q ≠ 0
hl : natDegree q < natDegree p
⊢ ¬p ∣ q
[PROOFSTEP]
rintro ⟨r, rfl⟩
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r✝ : R[X]
hp : Monic p
r : R[X]
h0 : p * r ≠ 0
hl : natDegree (p * r) < natDegree p
⊢ False
[PROOFSTEP]
rw [hp.natDegree_mul' <| right_ne_zero_of_mul h0] at hl 
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r✝ : R[X]
hp : Monic p
r : R[X]
h0 : p * r ≠ 0
hl : natDegree p + natDegree r < natDegree p
⊢ False
[PROOFSTEP]
exact hl.not_le (Nat.le_add_right _ _)
[GOAL]
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
⊢ nextCoeff (p * q) = nextCoeff p + nextCoeff q
[PROOFSTEP]
nontriviality
[GOAL]
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
✝ : Nontrivial R
⊢ nextCoeff (p * q) = nextCoeff p + nextCoeff q
[PROOFSTEP]
simp only [← coeff_one_reverse]
[GOAL]
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
✝ : Nontrivial R
⊢ coeff (reverse (p * q)) 1 = coeff (reverse p) 1 + coeff (reverse q) 1
[PROOFSTEP]
rw [reverse_mul]
[GOAL]
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
✝ : Nontrivial R
⊢ coeff (reverse p * reverse q) 1 = coeff (reverse p) 1 + coeff (reverse q) 1
[PROOFSTEP]
simp [coeff_mul, Nat.antidiagonal, hp.leadingCoeff, hq.leadingCoeff, add_comm, show Nat.succ 0 = 1 from rfl]
[GOAL]
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
✝ : Nontrivial R
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
[PROOFSTEP]
simp [coeff_mul, Nat.antidiagonal, hp.leadingCoeff, hq.leadingCoeff, add_comm, show Nat.succ 0 = 1 from rfl]
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
⊢ p = 1
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
⊢ p = 1
[PROOFSTEP]
have hdeg : p.degree = 0 :=
  by
  rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]
  · rw [hp.leadingCoeff, f.map_one]
    exact one_ne_zero
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
⊢ degree p = 0
[PROOFSTEP]
rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
⊢ ↑f (Polynomial.leadingCoeff p) ≠ 0
[PROOFSTEP]
rw [hp.leadingCoeff, f.map_one]
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
hdeg : degree p = 0
⊢ p = 1
[PROOFSTEP]
have hndeg : p.natDegree = 0 := WithBot.coe_eq_coe.mp ((degree_eq_natDegree hp.ne_zero).symm.trans hdeg)
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
hdeg : degree p = 0
hndeg : natDegree p = 0
⊢ p = 1
[PROOFSTEP]
convert eq_C_of_degree_eq_zero hdeg
[GOAL]
case h.e'_3
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
hdeg : degree p = 0
hndeg : natDegree p = 0
⊢ 1 = ↑C (coeff p 0)
[PROOFSTEP]
rw [← hndeg, ← Polynomial.leadingCoeff, hp.leadingCoeff, C.map_one]
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
n : ℕ
⊢ natDegree (p ^ n) = n * natDegree p
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ natDegree (p ^ Nat.zero) = Nat.zero * natDegree p
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
n : ℕ
hn : natDegree (p ^ n) = n * natDegree p
⊢ natDegree (p ^ Nat.succ n) = Nat.succ n * natDegree p
[PROOFSTEP]
rw [pow_succ, hp.natDegree_mul (hp.pow n), hn, Nat.succ_mul, add_comm]
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ natDegree ((X + ↑C r) ^ n) = n
[PROOFSTEP]
rw [(monic_X_add_C r).natDegree_pow, natDegree_X_add_C, mul_one]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hm : Monic p
hpu : IsUnit p
⊢ p = 1
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
⊢ p = 1
[PROOFSTEP]
obtain ⟨q, h⟩ := hpu.exists_right_inv
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
q : R[X]
h : p * q = 1
⊢ p = 1
[PROOFSTEP]
have := hm.natDegree_mul' (right_ne_zero_of_mul_eq_one h)
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : natDegree (p * q) = natDegree p + natDegree q
⊢ p = 1
[PROOFSTEP]
rw [h, natDegree_one, eq_comm, add_eq_zero_iff] at this 
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : natDegree p = 0 ∧ natDegree q = 0
⊢ p = 1
[PROOFSTEP]
exact hm.natDegree_eq_zero_iff_eq_one.mp this.1
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
ht : ∀ (i : ι), i ∈ t → Monic (f i)
⊢ Monic (Multiset.prod (Multiset.map f t))
[PROOFSTEP]
revert ht
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ (∀ (i : ι), i ∈ t → Monic (f i)) → Monic (Multiset.prod (Multiset.map f t))
[PROOFSTEP]
refine' t.induction_on _ _
[GOAL]
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ (∀ (i : ι), i ∈ 0 → Monic (f i)) → Monic (Multiset.prod (Multiset.map f 0))
[PROOFSTEP]
simp
[GOAL]
case refine'_2
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ ∀ ⦃a : ι⦄ {s : Multiset ι},
    ((∀ (i : ι), i ∈ s → Monic (f i)) → Monic (Multiset.prod (Multiset.map f s))) →
      (∀ (i : ι), i ∈ a ::ₘ s → Monic (f i)) → Monic (Multiset.prod (Multiset.map f (a ::ₘ s)))
[PROOFSTEP]
intro a t ih ht
[GOAL]
case refine'_2
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ (i : ι), i ∈ t → Monic (f i)) → Monic (Multiset.prod (Multiset.map f t))
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (Multiset.prod (Multiset.map f (a ::ₘ t)))
[PROOFSTEP]
rw [Multiset.map_cons, Multiset.prod_cons]
[GOAL]
case refine'_2
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ (i : ι), i ∈ t → Monic (f i)) → Monic (Multiset.prod (Multiset.map f t))
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (f a * Multiset.prod (Multiset.map f t))
[PROOFSTEP]
exact (ht _ (Multiset.mem_cons_self _ _)).mul (ih fun _ hi => ht _ (Multiset.mem_cons_of_mem hi))
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
h : ∀ (i : ι), i ∈ t → Monic (f i)
⊢ nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
[PROOFSTEP]
revert h
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
[PROOFSTEP]
refine' Multiset.induction_on t _ fun a t ih ht => _
[GOAL]
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ (∀ (i : ι), i ∈ 0 → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f 0)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) 0)
[PROOFSTEP]
simp only [Multiset.not_mem_zero, forall_prop_of_true, forall_prop_of_false, Multiset.map_zero, Multiset.prod_zero,
  Multiset.sum_zero, not_false_iff, forall_true_iff]
[GOAL]
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ nextCoeff 1 = 0
[PROOFSTEP]
rw [← C_1]
[GOAL]
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ nextCoeff (↑C 1) = 0
[PROOFSTEP]
rw [nextCoeff_C_eq_zero]
[GOAL]
case refine'_2
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ nextCoeff (Multiset.prod (Multiset.map f (a ::ₘ t))) =
    Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) (a ::ₘ t))
[PROOFSTEP]
rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, Monic.nextCoeff_mul, ih]
[GOAL]
case refine'_2
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ ∀ (i : ι), i ∈ t → Monic (f i)
case refine'_2.hp
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (f a)
case refine'_2.hq
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (Multiset.prod (Multiset.map f t))
[PROOFSTEP]
exacts [fun i hi => ht i (Multiset.mem_cons_of_mem hi), ht a (Multiset.mem_cons_self _ _),
  monic_multiset_prod_of_monic _ _ fun b bs => ht _ (Multiset.mem_cons_of_mem bs)]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
⊢ natDegree (Polynomial.map f P) = natDegree P
[PROOFSTEP]
refine' le_antisymm (natDegree_map_le _ _) (le_natDegree_of_ne_zero _)
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
⊢ coeff (Polynomial.map f P) (natDegree P) ≠ 0
[PROOFSTEP]
rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
⊢ degree (Polynomial.map f P) = degree P
[PROOFSTEP]
by_cases hP : P = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : P = 0
⊢ degree (Polynomial.map f P) = degree P
[PROOFSTEP]
simp [hP]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ degree (Polynomial.map f P) = degree P
[PROOFSTEP]
refine' le_antisymm (degree_map_le _ _) _
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ degree P ≤ degree (Polynomial.map f P)
[PROOFSTEP]
rw [degree_eq_natDegree hP]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ ↑(natDegree P) ≤ degree (Polynomial.map f P)
[PROOFSTEP]
refine' le_degree_of_ne_zero _
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ coeff (Polynomial.map f P) (natDegree P) ≠ 0
[PROOFSTEP]
rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h : p = 0
⊢ degree (map f p) = degree p
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h : ¬p = 0
⊢ ↑f (leadingCoeff p) ≠ 0
[PROOFSTEP]
rw [← f.map_zero]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h : ¬p = 0
⊢ ↑f (leadingCoeff p) ≠ ↑f 0
[PROOFSTEP]
exact mt hf.eq_iff.1 (mt leadingCoeff_eq_zero.1 h)
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ leadingCoeff (map f p) = ↑f (leadingCoeff p)
[PROOFSTEP]
unfold leadingCoeff
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ coeff (map f p) (natDegree (map f p)) = ↑f (coeff p (natDegree p))
[PROOFSTEP]
rw [coeff_map, natDegree_map_eq_of_injective hf p]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ nextCoeff (map f p) = ↑f (nextCoeff p)
[PROOFSTEP]
unfold nextCoeff
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ (if natDegree (map f p) = 0 then 0 else coeff (map f p) (natDegree (map f p) - 1)) =
    ↑f (if natDegree p = 0 then 0 else coeff p (natDegree p - 1))
[PROOFSTEP]
rw [natDegree_map_eq_of_injective hf]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ (if natDegree p = 0 then 0 else coeff (map f p) (natDegree p - 1)) =
    ↑f (if natDegree p = 0 then 0 else coeff p (natDegree p - 1))
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h✝ : natDegree p = 0
⊢ 0 = ↑f (if natDegree p = 0 then 0 else coeff p (natDegree p - 1))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h✝ : ¬natDegree p = 0
⊢ coeff (map f p) (natDegree p - 1) = ↑f (if natDegree p = 0 then 0 else coeff p (natDegree p - 1))
[PROOFSTEP]
simp [*]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ leadingCoeff (map f p) = ↑f (leadingCoeff p)
[PROOFSTEP]
delta leadingCoeff
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ coeff (map f p) (natDegree (map f p)) = ↑f (coeff p (natDegree p))
[PROOFSTEP]
rw [coeff_map f, natDegree_map_eq_of_injective hf p]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
hp : Monic (map f p)
⊢ Monic p
[PROOFSTEP]
apply hf
[GOAL]
case a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
hp : Monic (map f p)
⊢ ↑f (leadingCoeff p) = ↑f 1
[PROOFSTEP]
rw [← leadingCoeff_of_injective hf, hp.leadingCoeff, f.map_one]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p : R[X]
x : R
⊢ Monic (X - ↑C x)
[PROOFSTEP]
simpa only [sub_eq_add_neg, C_neg] using monic_X_add_C (-x)
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Ring R
p : R[X]
n : ℕ
H : degree p ≤ ↑n
⊢ Monic (X ^ (n + 1) - p)
[PROOFSTEP]
simpa [sub_eq_add_neg] using monic_X_pow_add (show degree (-p) ≤ n by rwa [← degree_neg p] at H )
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Ring R
p : R[X]
n : ℕ
H : degree p ≤ ↑n
⊢ degree (-p) ≤ ↑n
[PROOFSTEP]
rwa [← degree_neg p] at H 
[GOAL]
R✝ : Type u
S : Type v
a✝ b : R✝
m n✝ : ℕ
ι : Type y
inst✝¹ : Ring R✝
p : R✝[X]
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : n ≠ 0
⊢ Monic (X ^ n - ↑C a)
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
[GOAL]
case intro
R✝ : Type u
S : Type v
a✝ b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Ring R✝
p : R✝[X]
R : Type u
inst✝ : Ring R
a : R
k : ℕ
h : Nat.succ k ≠ 0
⊢ Monic (X ^ Nat.succ k - ↑C a)
[PROOFSTEP]
apply monic_X_pow_sub _
[GOAL]
R✝ : Type u
S : Type v
a✝ b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Ring R✝
p : R✝[X]
R : Type u
inst✝ : Ring R
a : R
k : ℕ
h : Nat.succ k ≠ 0
⊢ degree (↑C a) ≤ ↑k
[PROOFSTEP]
exact le_trans degree_C_le Nat.WithBot.coe_nonneg
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
m n✝ : ℕ
ι : Type y
inst✝² : Ring R✝
p : R✝[X]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
⊢ ¬IsUnit (X ^ n - 1)
[PROOFSTEP]
intro h
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
m n✝ : ℕ
ι : Type y
inst✝² : Ring R✝
p : R✝[X]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
⊢ False
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝² : Ring R✝
p : R✝[X]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : IsUnit (X ^ 0 - 1)
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
case inr
R✝ : Type u
S : Type v
a b : R✝
m n✝ : ℕ
ι : Type y
inst✝² : Ring R✝
p : R✝[X]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ False
[PROOFSTEP]
apply hn
[GOAL]
case inr
R✝ : Type u
S : Type v
a b : R✝
m n✝ : ℕ
ι : Type y
inst✝² : Ring R✝
p : R✝[X]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ n = 0
[PROOFSTEP]
rw [← @natDegree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, natDegree_X_pow_sub_C]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hp : Monic p
hpq : degree q < degree p
⊢ Monic (p - q)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hp : Monic p
hpq : degree q < degree p
⊢ Monic (p + -q)
[PROOFSTEP]
apply hp.add_of_left
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hp : Monic p
hpq : degree q < degree p
⊢ degree (-q) < degree p
[PROOFSTEP]
rwa [degree_neg]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
⊢ Monic (p - q)
[PROOFSTEP]
have : (-q).coeff (-q).natDegree = 1 := by rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
⊢ coeff (-q) (natDegree (-q)) = 1
[PROOFSTEP]
rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
this : coeff (-q) (natDegree (-q)) = 1
⊢ Monic (p - q)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
this : coeff (-q) (natDegree (-q)) = 1
⊢ Monic (p + -q)
[PROOFSTEP]
apply Monic.add_of_right this
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
this : coeff (-q) (natDegree (-q)) = 1
⊢ degree p < degree (-q)
[PROOFSTEP]
rwa [degree_neg]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
⊢ q * p ≠ 0
[PROOFSTEP]
by_cases h : p = 1
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ q * p ≠ 0
[PROOFSTEP]
simpa [h]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ q * p ≠ 0
[PROOFSTEP]
rw [Ne.def, ← degree_eq_bot, hp.degree_mul, WithBot.add_eq_bot, not_or, degree_eq_bot]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬degree p = ⊥
[PROOFSTEP]
refine' ⟨hq, _⟩
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬degree p = ⊥
[PROOFSTEP]
rw [← hp.degree_le_zero_iff_eq_one, not_le] at h 
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : 0 < degree p
⊢ ¬degree p = ⊥
[PROOFSTEP]
refine' (lt_trans _ h).ne'
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : 0 < degree p
⊢ ⊥ < 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
⊢ p * q ≠ 0
[PROOFSTEP]
by_cases h : p = 1
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ p * q ≠ 0
[PROOFSTEP]
simpa [h]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ p * q ≠ 0
[PROOFSTEP]
rw [Ne.def, ← degree_eq_bot, hp.degree_mul_comm, hp.degree_mul, WithBot.add_eq_bot, not_or, degree_eq_bot]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬degree p = ⊥
[PROOFSTEP]
refine' ⟨hq, _⟩
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬degree p = ⊥
[PROOFSTEP]
rw [← hp.degree_le_zero_iff_eq_one, not_le] at h 
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : 0 < degree p
⊢ ¬degree p = ⊥
[PROOFSTEP]
refine' (lt_trans _ h).ne'
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : 0 < degree p
⊢ ⊥ < 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
[PROOFSTEP]
suffices 0 < p.natDegree ↔ p.natDegree ≠ 0 by simpa [hq, ← h.natDegree_eq_zero_iff_eq_one]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
this : 0 < natDegree p ↔ natDegree p ≠ 0
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
[PROOFSTEP]
simpa [hq, ← h.natDegree_eq_zero_iff_eq_one]
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
⊢ 0 < natDegree p ↔ natDegree p ≠ 0
[PROOFSTEP]
exact ⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : ¬q = 0
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
[PROOFSTEP]
simp [h.natDegree_mul', hq]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
⊢ p * q = 0 ↔ q = 0
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
⊢ p * q = 0 ↔ q = 0
[PROOFSTEP]
simp [h.mul_right_ne_zero, hq]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : ¬q = 0
⊢ p * q = 0 ↔ q = 0
[PROOFSTEP]
simp [h.mul_right_ne_zero, hq]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
⊢ q * p = 0 ↔ q = 0
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
⊢ q * p = 0 ↔ q = 0
[PROOFSTEP]
simp [h.mul_left_ne_zero, hq]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : ¬q = 0
⊢ q * p = 0 ↔ q = 0
[PROOFSTEP]
simp [h.mul_left_ne_zero, hq]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
⊢ IsRegular p
[PROOFSTEP]
constructor
[GOAL]
case left
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
⊢ IsLeftRegular p
[PROOFSTEP]
intro q r h
[GOAL]
case left
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : (fun x => p * x) q = (fun x => p * x) r
⊢ q = r
[PROOFSTEP]
dsimp only at h 
[GOAL]
case left
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : p * q = p * r
⊢ q = r
[PROOFSTEP]
rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]
[GOAL]
case right
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
⊢ IsRightRegular p
[PROOFSTEP]
intro q r h
[GOAL]
case right
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : (fun x => x * p) q = (fun x => x * p) r
⊢ q = r
[PROOFSTEP]
simp only at h 
[GOAL]
case right
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : q * p = r * p
⊢ q = r
[PROOFSTEP]
rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ degree (k • p) = degree p
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ degree (k • p) ≤ degree p
[PROOFSTEP]
rw [degree_le_iff_coeff_zero]
[GOAL]
case refine'_1
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ ∀ (m : ℕ), degree p < ↑m → coeff (k • p) m = 0
[PROOFSTEP]
intro m hm
[GOAL]
case refine'_1
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : degree p < ↑m
⊢ coeff (k • p) m = 0
[PROOFSTEP]
rw [degree_lt_iff_coeff_zero] at hm 
[GOAL]
case refine'_1
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff p m_1 = 0
⊢ coeff (k • p) m = 0
[PROOFSTEP]
simp [hm m le_rfl]
[GOAL]
case refine'_2
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ degree p ≤ degree (k • p)
[PROOFSTEP]
rw [degree_le_iff_coeff_zero]
[GOAL]
case refine'_2
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ ∀ (m : ℕ), degree (k • p) < ↑m → coeff p m = 0
[PROOFSTEP]
intro m hm
[GOAL]
case refine'_2
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : degree (k • p) < ↑m
⊢ coeff p m = 0
[PROOFSTEP]
rw [degree_lt_iff_coeff_zero] at hm 
[GOAL]
case refine'_2
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff (k • p) m_1 = 0
⊢ coeff p m = 0
[PROOFSTEP]
refine' h _
[GOAL]
case refine'_2
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff (k • p) m_1 = 0
⊢ (fun x => k • x) (coeff p m) = (fun x => k • x) 0
[PROOFSTEP]
simpa using hm m le_rfl
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ natDegree (k • p) = natDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : p = 0
⊢ natDegree (k • p) = natDegree p
[PROOFSTEP]
simp [hp]
[GOAL]
case neg
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ natDegree (k • p) = natDegree p
[PROOFSTEP]
rw [← WithBot.coe_eq_coe, ← Nat.cast_withBot, ← Nat.cast_withBot, ← degree_eq_natDegree hp, ← degree_eq_natDegree,
  degree_smul_of_smul_regular p h]
[GOAL]
case neg
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ k • p ≠ 0
[PROOFSTEP]
contrapose! hp
[GOAL]
case neg
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = 0
⊢ p = 0
[PROOFSTEP]
rw [← smul_zero k] at hp 
[GOAL]
case neg
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp✝ : k • p = 0
hp : k • p = k • 0
⊢ p = 0
[PROOFSTEP]
exact h.polynomial hp
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ leadingCoeff (k • p) = k • leadingCoeff p
[PROOFSTEP]
rw [Polynomial.leadingCoeff, Polynomial.leadingCoeff, coeff_smul, natDegree_smul_of_smul_regular p h]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
⊢ Monic ((IsUnit.unit h)⁻¹ • p)
[PROOFSTEP]
rw [Monic.def, leadingCoeff_smul_of_smul_regular _ (isSMulRegular_of_group _), Units.smul_def]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
⊢ ↑(IsUnit.unit h)⁻¹ • leadingCoeff p = 1
[PROOFSTEP]
obtain ⟨k, hk⟩ := h
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
k : Rˣ
hk : ↑k = leadingCoeff p
⊢ ↑(IsUnit.unit (_ : ∃ u, ↑u = leadingCoeff p))⁻¹ • leadingCoeff p = 1
[PROOFSTEP]
simp only [← hk, smul_eq_mul, ← Units.val_mul, Units.val_eq_one, inv_mul_eq_iff_eq_mul]
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
k : Rˣ
hk : ↑k = leadingCoeff p
⊢ k = IsUnit.unit (_ : IsUnit ↑k) * 1
[PROOFSTEP]
simp [Units.ext_iff, IsUnit.unit_spec]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
intro hp
[GOAL]
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
[PROOFSTEP]
rw [← smul_eq_zero_iff_eq h.unit⁻¹] at hp 
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]
ext
[GOAL]
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✝
[PROOFSTEP]
simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
[GOAL]
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
[PROOFSTEP]
refine' sum_congr rfl fun x _ => _
[GOAL]
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
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
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
[PROOFSTEP]
rwa [this, Monic.mul_right_eq_zero_iff] at hp 
[GOAL]
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)
[PROOFSTEP]
exact monic_of_isUnit_leadingCoeff_inv_smul _
[GOAL]
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
[PROOFSTEP]
rintro rfl
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
intro hp
[GOAL]
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
[PROOFSTEP]
replace hp := congr_arg (· * C ↑h.unit⁻¹) hp
[GOAL]
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
[PROOFSTEP]
simp only [zero_mul] at hp 
[GOAL]
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
[PROOFSTEP]
rwa [mul_assoc, Monic.mul_left_eq_zero_iff] at hp 
[GOAL]
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)⁻¹)
[PROOFSTEP]
refine' monic_mul_C_of_leadingCoeff_mul_eq_one _
[GOAL]
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
[PROOFSTEP]
simp [Units.mul_inv_eq_iff_eq_mul, IsUnit.unit_spec]
[GOAL]
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
[PROOFSTEP]
rintro rfl
[GOAL]
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
[PROOFSTEP]
rw [zero_mul]
