p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ 0 = Polynomial.eval (z' - a + a) F
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ 0 = Polynomial.eval (a + (z' - a)) F
rw [add_comm]
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ 0 = Polynomial.eval (z' - a + a) F
simp [hz']
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ Polynomial.eval (a + h) F = Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
rw [hq, ha, zero_add]
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2 =
    (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h
rw [sq, right_distrib, mul_assoc]
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
⊢ Polynomial.eval a (↑Polynomial.derivative F) = -q * h
simpa using eq_neg_of_add_eq_zero_left this
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ = ‖q‖ * ‖h‖
simp [this]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ ‖q‖ ≤ 1
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ ‖q‖ * ‖h‖ ≤ 1 * ‖h‖
gcongr
no goals
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ ‖q‖ ≤ 1
apply PadicInt.norm_le_one
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ 1 * ‖h‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
simpa
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
this : h = 0
⊢ z' - a = 0
rw [← this]