Commit 2023-03-22 07:28 1d7f4d20

View on Github →

feat: port NumberTheory.Padics.PadicVal (#3020)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Padics/PadicVal.lean

added theorem dvd_iff_padicValNat_ne_zero

added theorem dvd_of_one_le_padicValNat

added theorem one_le_padicValNat_of_dvd

added theorem padicValInt.eq_zero_of_not_dvd

added theorem padicValInt.mul

added theorem padicValInt.of_nat

added theorem padicValInt.of_ne_one_ne_zero

added theorem padicValInt.self

added def padicValInt

added theorem padicValInt_dvd

added theorem padicValInt_dvd_iff

added theorem padicValInt_mul_eq_succ

added theorem padicValInt_self

added theorem padicValNat.eq_zero_iff

added theorem padicValNat.eq_zero_of_not_dvd

added theorem padicValNat.self

added def padicValNat

added theorem padicValNat_def'

added theorem padicValNat_def

added theorem padicValNat_dvd_iff

added theorem padicValNat_dvd_iff_le

added theorem padicValNat_primes

added theorem padicValNat_self

added theorem padicValRat.finite_int_prime_iff

added theorem padicValRat.le_padicValRat_add_of_le

added theorem padicValRat.min_le_padicValRat_add

added theorem padicValRat.multiplicity_sub_multiplicity

added theorem padicValRat.of_int

added theorem padicValRat.of_int_multiplicity

added theorem padicValRat.of_nat

added theorem padicValRat.padicValRat_le_padicValRat_iff

added theorem padicValRat.self

added theorem padicValRat.sum_pos_of_pos

added def padicValRat

added theorem padicValRat_of_nat

added theorem pow_padicValNat_dvd

added theorem pow_succ_padicValNat_not_dvd

added theorem range_pow_padicValNat_subset_divisors'

added theorem range_pow_padicValNat_subset_divisors

added theorem zero_le_padicValRat_of_nat