Commit 2023-05-25 12:49 63d78da6

View on Github →

feat: port NumberTheory.Padics.PadicIntegers (#4269)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Padics/PadicIntegers.lean

added def PadicInt.Coe.ringHom

added theorem PadicInt.algebraMap_apply

added theorem PadicInt.coe_add

added theorem PadicInt.coe_eq_zero

added theorem PadicInt.coe_int_cast

added theorem PadicInt.coe_int_eq

added theorem PadicInt.coe_mul

added theorem PadicInt.coe_nat_cast

added theorem PadicInt.coe_ne_zero

added theorem PadicInt.coe_neg

added theorem PadicInt.coe_one

added theorem PadicInt.coe_pow

added theorem PadicInt.coe_sub

added theorem PadicInt.coe_zero

added theorem PadicInt.exists_pow_neg_lt

added theorem PadicInt.exists_pow_neg_lt_rat

added theorem PadicInt.ext

added theorem PadicInt.ideal_eq_span_pow_p

added def PadicInt.inv

added theorem PadicInt.inv_mul

added theorem PadicInt.irreducible_p

added theorem PadicInt.isUnit_iff

added theorem PadicInt.maximalIdeal_eq_span_p

added theorem PadicInt.mem_nonunits

added theorem PadicInt.mem_span_pow_iff_le_valuation

added theorem PadicInt.mem_subring_iff

added def PadicInt.mkUnits

added theorem PadicInt.mkUnits_eq

added theorem PadicInt.mk_coe

added theorem PadicInt.mk_zero

added theorem PadicInt.mul_inv

added theorem PadicInt.nonarchimedean

added theorem PadicInt.norm_add_eq_max_of_ne

added theorem PadicInt.norm_def

added theorem PadicInt.norm_eq_of_norm_add_lt_left

added theorem PadicInt.norm_eq_of_norm_add_lt_right

added theorem PadicInt.norm_eq_padic_norm

added theorem PadicInt.norm_eq_pow_val

added theorem PadicInt.norm_int_cast_eq_padic_norm

added theorem PadicInt.norm_int_le_pow_iff_dvd

added theorem PadicInt.norm_int_lt_one_iff_dvd

added theorem PadicInt.norm_le_one

added theorem PadicInt.norm_le_pow_iff_le_valuation

added theorem PadicInt.norm_le_pow_iff_mem_span_pow

added theorem PadicInt.norm_le_pow_iff_norm_lt_pow_add_one

added theorem PadicInt.norm_lt_one_add

added theorem PadicInt.norm_lt_one_iff_dvd

added theorem PadicInt.norm_lt_one_mul

added theorem PadicInt.norm_lt_pow_iff_norm_le_pow_sub_one

added theorem PadicInt.norm_mul

added theorem PadicInt.norm_p

added theorem PadicInt.norm_p_pow

added theorem PadicInt.norm_pow

added theorem PadicInt.norm_units

added def PadicInt.ofIntSeq

added theorem PadicInt.p_nonnunit

added theorem PadicInt.padic_norm_e_of_padicInt

added theorem PadicInt.pow_p_dvd_int_iff

added theorem PadicInt.prime_p

added def PadicInt.subring

added def PadicInt.unitCoeff

added theorem PadicInt.unitCoeff_coe

added theorem PadicInt.unitCoeff_spec

added def PadicInt.valuation

added theorem PadicInt.valuation_nonneg

added theorem PadicInt.valuation_one

added theorem PadicInt.valuation_p

added theorem PadicInt.valuation_p_pow_mul

added theorem PadicInt.valuation_zero

added def PadicInt