Commit 2023-05-22 00:38 bd1295bb

View on Github →

feat: port NumberTheory.Padics.PadicNumbers (#3095)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Field/Basic.lean

added theorem add_thirds

Created Mathlib/NumberTheory/Padics/PadicNumbers.lean

added theorem Padic.AddValuation.map_add

added theorem Padic.AddValuation.map_mul

added theorem Padic.AddValuation.map_one

added theorem Padic.AddValuation.map_zero

added theorem Padic.addValuation.apply

added def Padic.addValuation

added def Padic.addValuationDef

added theorem Padic.coe_add

added theorem Padic.coe_div

added theorem Padic.coe_inj

added theorem Padic.coe_mul

added theorem Padic.coe_neg

added theorem Padic.coe_one

added theorem Padic.coe_sub

added theorem Padic.coe_zero

added theorem Padic.complete''

added theorem Padic.complete'

added theorem Padic.const_equiv

added theorem Padic.exi_rat_seq_conv

added theorem Padic.exi_rat_seq_conv_cauchy

added def Padic.limSeq

added def Padic.mk

added theorem Padic.mk_eq

added theorem Padic.norm_eq_pow_val

added theorem Padic.norm_le_one_iff_val_nonneg

added theorem Padic.norm_le_pow_iff_norm_lt_pow_add_one

added theorem Padic.norm_lt_pow_iff_norm_le_pow_sub_one

added theorem Padic.padicNormE_lim_le

added theorem Padic.rat_dense'

added theorem Padic.rat_dense

added def Padic.valuation

added theorem Padic.valuation_map_add

added theorem Padic.valuation_map_mul

added theorem Padic.valuation_one

added theorem Padic.valuation_p

added theorem Padic.valuation_zero

added theorem Padic.zero_def

added def Padic

added theorem PadicSeq.add_eq_max_of_ne

added theorem PadicSeq.eq_zero_iff_equiv_zero

added theorem PadicSeq.equiv_zero_of_val_eq_of_equiv_zero

added theorem PadicSeq.lift_index_left

added theorem PadicSeq.lift_index_left_left

added theorem PadicSeq.lift_index_right

added theorem PadicSeq.ne_zero_iff_nequiv_zero

added def PadicSeq.norm

added theorem PadicSeq.norm_const

added theorem PadicSeq.norm_eq

added theorem PadicSeq.norm_eq_norm_app_of_nonzero

added theorem PadicSeq.norm_eq_of_add_equiv_zero

added theorem PadicSeq.norm_eq_pow_val

added theorem PadicSeq.norm_equiv

added theorem PadicSeq.norm_mul

added theorem PadicSeq.norm_neg

added theorem PadicSeq.norm_nonarchimedean

added theorem PadicSeq.norm_nonneg

added theorem PadicSeq.norm_nonzero_of_not_equiv_zero

added theorem PadicSeq.norm_one

added theorem PadicSeq.norm_values_discrete

added theorem PadicSeq.norm_zero_iff

added theorem PadicSeq.not_equiv_zero_const_of_nonzero

added theorem PadicSeq.not_limZero_const_of_nonzero

added theorem PadicSeq.stationary

added def PadicSeq.stationaryPoint

added theorem PadicSeq.stationaryPoint_spec

added theorem PadicSeq.val_eq_iff_norm_eq

added def PadicSeq.valuation

added def PadicSeq

added theorem padicNormE.add_eq_max_of_ne'

added theorem padicNormE.add_eq_max_of_ne

added theorem padicNormE.defn

added theorem padicNormE.eq_of_norm_add_lt_left

added theorem padicNormE.eq_of_norm_add_lt_right

added theorem padicNormE.eq_padicNorm

added theorem padicNormE.eq_padic_norm'

added theorem padicNormE.eq_ratNorm

added theorem padicNormE.nonarchimedean'

added theorem padicNormE.nonarchimedean

added theorem padicNormE.norm_int_le_one

added theorem padicNormE.norm_int_le_pow_iff_dvd

added theorem padicNormE.norm_int_lt_one_iff_dvd

added theorem padicNormE.norm_p

added theorem padicNormE.norm_p_lt_one

added theorem padicNormE.norm_p_pow

added theorem padicNormE.norm_p_zpow

added theorem padicNormE.norm_rat_le_one

added def padicNormE.ratNorm

added def padicNormE

Modified Mathlib/RingTheory/Valuation/Basic.lean