Theorem norm_natAbs

Modification history

2025-08-25 03:00

Mathlib/Analysis/Normed/Ring/Basic.lean

feat(NumberTheory/Padics): norm of Int lt one iff p divides (#27958) …

Added norm_natAbs View on Github →