Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-02 14:02 f040aef2

View on Github →

feat(data/padics): use has_norm typeclasses for padics

Estimated changes

Modified algebra/archimedean.lean

modified theorem ceil_nonneg

added theorem ceil_zero

Modified algebra/field_power.lean

Modified analysis/normed_space.lean

added theorem norm_div

added theorem norm_inv

added theorem norm_one

added theorem norm_sub_rev

Modified data/int/basic.lean

added theorem int.dvd_of_pow_dvd

deleted theorem int.pow_div_of_le_of_pow_div_int

added theorem int.pow_dvd_of_le_of_pow_dvd

Modified data/nat/basic.lean

added theorem nat.div_mul_div

added theorem nat.dvd_of_pow_dvd

deleted theorem nat.nat.div_mul_div

deleted theorem nat.pow_div_of_le_of_pow_div

added theorem nat.pow_dvd_of_le_of_pow_dvd

Modified data/padics/padic_integers.lean

added theorem padic_int.add_def

added theorem padic_int.coe_add

added theorem padic_int.coe_coe

added theorem padic_int.coe_mul

added theorem padic_int.coe_neg

added theorem padic_int.coe_one

added theorem padic_int.coe_sub

added def padic_int.inv

added theorem padic_int.inv_mul

added def padic_int.maximal_ideal

added theorem padic_int.maximal_ideal_add

added theorem padic_int.maximal_ideal_eq_nonunits

added theorem padic_int.maximal_ideal_eq_or_univ_of_subset

added theorem padic_int.maximal_ideal_mul

added theorem padic_int.maximal_ideal_ne_univ

added theorem padic_int.maximal_ideal_unique

added theorem padic_int.mk_coe

added theorem padic_int.mk_zero

added theorem padic_int.mul_def

added theorem padic_int.mul_inv

added theorem padic_int.val_eq_coe

added theorem padic_int.zero_def

modified def padic_int

added theorem padic_norm_z.le_one

added theorem padic_norm_z.mul

added theorem padic_norm_z.nonarchimedean

added theorem padic_norm_z.norm_one

added def padic_norm_z

Modified data/padics/padic_norm.lean

added theorem padic_val.dvd_of_padic_val_pos

deleted theorem padic_val.le_padic_val_of_pow_div

added theorem padic_val.le_padic_val_of_pow_dvd

added theorem padic_val.padic_val_eq_zero_of_coprime

added theorem padic_val.padic_val_eq_zero_of_not_dvd'

added theorem padic_val.padic_val_eq_zero_of_not_dvd

Modified data/padics/padic_rationals.lean

added theorem padic.complete'

deleted theorem padic.complete

modified def padic.lim_seq

added theorem padic.rat_dense'

modified theorem padic.rat_dense

modified def padic

added theorem padic_norm_e.eq_padic_norm'

modified theorem padic_norm_e.eq_padic_norm

added theorem padic_norm_e.eq_rat_norm

added theorem padic_norm_e.nonarchimedean'

modified theorem padic_norm_e.nonarchimedean

added def padic_norm_e.rat_norm

added theorem padic_norm_e.triangle_ineq

modified theorem padic_seq.norm_equiv

modified theorem padic_seq.norm_mul