Commit 2023-03-24 11:58 ce36bd4a

View on Github →

feat: port NumberTheory.Padics.PadicNorm (#3069)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Padics/PadicNorm.lean

added theorem padicNorm.add_eq_max_of_ne

added theorem padicNorm.dvd_iff_norm_le

added theorem padicNorm.int_eq_one_iff

added theorem padicNorm.int_lt_one_iff

added theorem padicNorm.nat_eq_one_iff

added theorem padicNorm.nat_lt_one_iff

added theorem padicNorm.of_nat

added theorem padicNorm.padicNorm_of_prime_of_ne

added theorem padicNorm.padicNorm_p

added theorem padicNorm.padicNorm_p_lt_one

added theorem padicNorm.padicNorm_p_lt_one_of_prime

added theorem padicNorm.padicNorm_p_of_prime

added theorem padicNorm.sum_le'

added theorem padicNorm.sum_le

added theorem padicNorm.sum_lt'

added theorem padicNorm.sum_lt

added theorem padicNorm.triangle_ineq

added theorem padicNorm.zero_of_padicNorm_eq_zero

added def padicNorm