no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖Polynomial.eval x F - Polynomial.eval y F‖ = ‖z‖ * ‖x - y‖
simp [hz]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖z‖ ≤ 1
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖z‖ * ‖x - y‖ ≤ 1 * ‖x - y‖
gcongr
no goals
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖z‖ ≤ 1
apply PadicInt.norm_le_one
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ 1 * ‖x - y‖ = ‖x - y‖
simp