case inl
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
h : ↑derivative 0 = 0
⊢ natDegree 0 = 0

case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
⊢ natDegree f = 0
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
⊢ natDegree f = 0
rcases eq_or_ne f 0 with (rfl | hf)
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
⊢ degree f ≤ 0
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
⊢ natDegree f = 0
rw [natDegree_eq_zero_iff_degree_le_zero]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < degree f
⊢ False
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
⊢ degree f ≤ 0
by_contra' f_nat_degree_pos
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
⊢ False
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < degree f
⊢ False
rw [← natDegree_pos_iff_degree_pos] at f_nat_degree_pos
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
⊢ False
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
⊢ False
let m := f.natDegree - 1
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
⊢ False
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
⊢ False
have hm : m + 1 = f.natDegree := tsub_add_cancel_of_le f_nat_degree_pos
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : coeff (↑derivative f) m = coeff f (m + 1) * (↑m + 1)
⊢ False
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
⊢ False
have h2 := coeff_derivative f m
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), coeff (↑derivative f) n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : coeff (↑derivative f) m = coeff f (m + 1) * (↑m + 1)
⊢ False
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ↑derivative f = 0
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : coeff (↑derivative f) m = coeff f (m + 1) * (↑m + 1)
⊢ False
rw [Polynomial.ext_iff] at h
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), coeff (↑derivative f) n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : m + 1 = 0 ∨ coeff f (m + 1) = 0
⊢ False
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), coeff (↑derivative f) n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : coeff (↑derivative f) m = coeff f (m + 1) * (↑m + 1)
⊢ False
rw [h m, coeff_zero, ← Nat.cast_add_one, ← nsmul_eq_mul', eq_comm, smul_eq_zero] at h2
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), coeff (↑derivative f) n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : coeff f (m + 1) = 0
⊢ False
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), coeff (↑derivative f) n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : m + 1 = 0 ∨ coeff f (m + 1) = 0
⊢ False
replace h2 := h2.resolve_left m.succ_ne_zero
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), coeff (↑derivative f) n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : f = 0
⊢ False
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), coeff (↑derivative f) n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : coeff f (m + 1) = 0
⊢ False
rw [hm, ← leadingCoeff, leadingCoeff_eq_zero] at h2
no goals
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
f : R[X]
h : ∀ (n : ℕ), coeff (↑derivative f) n = coeff 0 n
hf : f ≠ 0
f_nat_degree_pos : 0 < natDegree f
m : ℕ := natDegree f - 1
hm : m + 1 = natDegree f
h2 : f = 0
⊢ False
exact hf h2
no goals
case inl
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
h : ↑derivative 0 = 0
⊢ natDegree 0 = 0
exact natDegree_zero