mathlib3

ee78812f - feat(number_theory/padics/padic_norm): lemmas (#10765)