mathlib3

51b175cf - feat(number_theory/padics/padic_norm): add int_eq_one_iff (#16074)

feat(number_theory/padics/padic_norm): add int_eq_one_iff (#16074) Add the proof that the p-adic norm of an integer is 1 iff the integer is not a multiple of p and related API for `padic_norm`.