Prove2Me

P_adic_Norm_is_Norm

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

normsnumber-theoryp-adicproofwiki

The p-adic norm forms a norm on the rational numbers Q.

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.NumberTheory.Padics.PadicNorm
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.NumberTheory.Padics.PadicNorm

theorem P_adic_Norm_is_Norm (p : ℕ) [hp : Fact (Nat.Prime p)] : IsAbsoluteValue (padicNorm p) := by sorry
Source
https://proofwiki.org/wiki/P-adic_Norm_is_Norm

View graph