Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-02 14:08 1562cc2c

View on Github →

feat(data/padics): use prime typeclass

Estimated changes

Created analysis/polynomial.lean

added theorem polynomial.continuous_eval

Modified data/padics/hensel.lean

modified theorem hensels_lemma

modified theorem limit_zero_of_norm_tendsto_zero

modified theorem padic_polynomial_dist

Modified data/padics/padic_integers.lean

modified def padic_int.add

modified theorem padic_int.add_def

modified theorem padic_int.cast_pow

deleted def padic_int.cau_seq_lim

deleted theorem padic_int.cau_seq_lim_spec

modified theorem padic_int.coe_add

modified theorem padic_int.coe_coe

modified theorem padic_int.coe_mul

modified theorem padic_int.coe_neg

modified theorem padic_int.coe_one

modified theorem padic_int.coe_sub

modified theorem padic_int.coe_zero

modified def padic_int.inv

modified theorem padic_int.inv_mul

modified def padic_int.maximal_ideal

modified theorem padic_int.maximal_ideal_add

modified theorem padic_int.maximal_ideal_eq_nonunits

modified theorem padic_int.maximal_ideal_eq_or_univ_of_subset

modified theorem padic_int.maximal_ideal_mul

modified theorem padic_int.maximal_ideal_ne_univ

modified theorem padic_int.maximal_ideal_unique

modified theorem padic_int.mk_coe

modified theorem padic_int.mk_zero

modified def padic_int.mul

modified theorem padic_int.mul_def

modified theorem padic_int.mul_inv

modified def padic_int.neg

deleted theorem padic_int.tendsto_limit

modified theorem padic_int.val_eq_coe

modified theorem padic_int.zero_def

modified def padic_int

modified theorem padic_norm_z.add_eq_max_of_ne

modified theorem padic_norm_z.eq_of_norm_add_lt_left

modified theorem padic_norm_z.eq_of_norm_add_lt_right

modified theorem padic_norm_z.le_one

modified theorem padic_norm_z.mul

modified theorem padic_norm_z.nonarchimedean

modified theorem padic_norm_z.norm_one

modified theorem padic_norm_z.one

modified theorem padic_norm_z.padic_norm_e_of_padic_int

modified theorem padic_norm_z.padic_norm_z_eq_padic_norm_e

modified theorem padic_norm_z.pow

modified def padic_norm_z

Modified data/padics/padic_norm.lean

modified theorem padic_norm.add_eq_max_of_ne

modified theorem padic_norm.le_of_dvd

modified theorem padic_norm.triangle_ineq

modified theorem padic_norm.zero_of_padic_norm_eq_zero

modified def padic_norm

Modified data/padics/padic_numbers.lean

modified theorem padic.cast_eq_of_rat

modified theorem padic.cast_eq_of_rat_of_int

modified theorem padic.cast_eq_of_rat_of_nat

deleted def padic.cau_seq_lim

deleted theorem padic.cau_seq_lim_spec

modified theorem padic.complete'

modified theorem padic.const_equiv

modified theorem padic.exi_rat_seq_conv_cauchy

modified def padic.mk

modified theorem padic.mk_eq

modified def padic.of_rat

modified theorem padic.of_rat_add

modified theorem padic.of_rat_div

modified theorem padic.of_rat_eq

modified theorem padic.of_rat_mul

modified theorem padic.of_rat_neg

modified theorem padic.of_rat_one

modified theorem padic.of_rat_sub

modified theorem padic.of_rat_zero

modified theorem padic.padic_norm_e_lim_le

modified theorem padic.rat_dense'

modified theorem padic.rat_dense

deleted theorem padic.tendsto_limit

modified def padic

modified theorem padic_norm_e.add_eq_max_of_ne'

modified theorem padic_norm_e.add_eq_max_of_ne

modified theorem padic_norm_e.defn

modified theorem padic_norm_e.eq_of_norm_add_lt_left

modified theorem padic_norm_e.eq_of_norm_add_lt_right

modified theorem padic_norm_e.eq_padic_norm'

modified theorem padic_norm_e.eq_padic_norm

modified theorem padic_norm_e.eq_rat_norm

modified theorem padic_norm_e.nonarchimedean'

modified theorem padic_norm_e.nonarchimedean

modified theorem padic_norm_e.norm_rat_le_one

modified def padic_norm_e.rat_norm

modified theorem padic_norm_e.sub_rev

modified theorem padic_norm_e.triangle_ineq

modified theorem padic_norm_e.zero_def

modified theorem padic_norm_e.zero_iff

modified def padic_norm_e

modified theorem padic_seq.add_eq_max_of_ne

modified theorem padic_seq.eq_zero_iff_equiv_zero

modified theorem padic_seq.equiv_zero_of_val_eq_of_equiv_zero

modified theorem padic_seq.lift_index_left

modified theorem padic_seq.lift_index_left_left

modified theorem padic_seq.lift_index_right

modified theorem padic_seq.ne_zero_iff_nequiv_zero

modified def padic_seq.norm

modified theorem padic_seq.norm_const

modified theorem padic_seq.norm_eq

modified theorem padic_seq.norm_eq_norm_app_of_nonzero

modified theorem padic_seq.norm_eq_of_add_equiv_zero

modified theorem padic_seq.norm_equiv

modified theorem padic_seq.norm_image

modified theorem padic_seq.norm_mul

modified theorem padic_seq.norm_neg

modified theorem padic_seq.norm_nonarchimedean

modified theorem padic_seq.norm_nonneg

modified theorem padic_seq.norm_nonzero_of_not_equiv_zero

modified theorem padic_seq.norm_one

modified theorem padic_seq.norm_zero_iff

modified theorem padic_seq.not_equiv_zero_const_of_nonzero

modified theorem padic_seq.not_lim_zero_const_of_nonzero

modified theorem padic_seq.stationary

modified def padic_seq.stationary_point

modified theorem padic_seq.stationary_point_spec

modified def padic_seq

Modified data/polynomial.lean

deleted theorem polynomial.continuous_eval

Modified data/real/basic.lean

modified theorem real.lim_add

modified theorem real.lim_const

modified theorem real.lim_eq_lim_of_equiv

modified theorem real.lim_mul_lim

Modified data/real/cau_seq.lean

added theorem cau_seq.lim_zero_sub_rev

Modified data/real/cau_seq_completion.lean

added theorem cau_seq.complete

added theorem cau_seq.lim_spec

Modified data/real/cau_seq_filter.lean

modified theorem cau_filter_lim_spec

deleted theorem cau_seq_lim_spec

deleted theorem complete_space_of_cauchy_complete

added theorem le_nhds_cau_filter_lim

deleted theorem le_nhds_cau_seq_lim

modified theorem set_seq_of_cau_filter_monotone

added theorem tendsto_limit