From 18ac3058155b1766ff1fc98e23c064c8d5b8fb25 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 10 Dec 2024 14:11:37 +0000 Subject: [PATCH] simp nf --- Mathlib/NumberTheory/Padics/PadicIntegers.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/Mathlib/NumberTheory/Padics/PadicIntegers.lean b/Mathlib/NumberTheory/Padics/PadicIntegers.lean index 9e0537b190001..71b2678ffc3bb 100644 --- a/Mathlib/NumberTheory/Padics/PadicIntegers.lean +++ b/Mathlib/NumberTheory/Padics/PadicIntegers.lean @@ -339,11 +339,6 @@ lemma le_valuation_add (hxy : x + y ≠ 0) : min x.valuation y.valuation ≤ (x lemma valuation_pow (x : ℤ_[p]) (n : ℕ) : (x ^ n).valuation = n * x.valuation := by zify; simp [← valuation_coe] -@[simp] -lemma valuation_zpow (x : ℚ_[p]) : ∀ n : ℤ, (x ^ n).valuation = n * x.valuation - | (n : ℕ) => by simp - | .negSucc n => by simp [← neg_mul]; simp [Int.negSucc_eq] - lemma norm_eq_zpow_neg_valuation {x : ℤ_[p]} (hx : x ≠ 0) : ‖x‖ = p ^ (-x.valuation : ℤ) := by simp [norm_def, Padic.norm_eq_zpow_neg_valuation <| coe_ne_zero.2 hx]