Commit 2022-09-03 10:46 51b175cf

View on Github →

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.

Estimated changes

Modified src/number_theory/padics/padic_norm.lean

added theorem padic_norm.int_eq_one_iff

added theorem padic_norm.int_lt_one_iff

added theorem padic_norm.nat_eq_one_iff

added theorem padic_norm.nat_lt_one_iff

added theorem padic_norm.of_nat

added theorem padic_norm.sum_le'

added theorem padic_norm.sum_le

added theorem padic_norm.sum_lt'

added theorem padic_norm.sum_lt