p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ‖x‖ = ↑p ^ (-valuation x)
refine @Padic.norm_eq_pow_val p hp x ?_
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ↑x = 0
⊢ x = 0
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x ≠ 0
contrapose! hx
no goals
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ↑x = 0
⊢ x = 0
exact Subtype.val_injective hx