Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-02 14:08 e0b0c537

View on Github →

feat(data/padics): prove Hensel's lemma

Estimated changes

Modified algebra/field_power.lean

added theorem fpow_ge_one_of_nonneg

added theorem fpow_le_one_of_nonpos

added theorem fpow_neg

added theorem fpow_pos_of_pos

added theorem fpow_sub

added theorem one_lt_fpow

added theorem one_lt_pow

Modified algebra/group_power.lean

added theorem div_sq_cancel

added theorem neg_square

added theorem pow_le_pow_of_le_left

added theorem pow_le_pow_of_le_one

added theorem pow_lt_pow_of_lt_one

Modified algebra/ordered_ring.lean

added theorem mul_le_iff_le_one_left

added theorem mul_le_iff_le_one_right

added theorem mul_lt_iff_lt_one_left

added theorem mul_lt_iff_lt_one_right

Modified analysis/limits.lean

added theorem tendsto_coe_iff

added theorem tendsto_pow_at_top_at_top_of_gt_1_nat

Modified analysis/normed_space.lean

modified theorem norm_div

modified theorem norm_inv

modified theorem norm_one

added theorem norm_pow

added theorem normed_field.norm_pow

Modified analysis/topology/topological_structures.lean

added theorem continuous_pow

Modified data/finsupp.lean

added theorem finsupp.sum_sub

Modified data/int/modeq.lean

added theorem int.modeq.exists_unique_equiv

added theorem int.modeq.exists_unique_equiv_nat

added theorem int.modeq.mod_coprime

added theorem int.modeq.modeq_add_fac

Modified data/nat/basic.lean

modified theorem nat.dvd_of_pow_dvd

added theorem nat.exists_eq_add_of_le

added theorem nat.exists_eq_add_of_lt

Created data/padics/default.lean

Created data/padics/hensel.lean

added theorem hensels_lemma

added theorem limit_zero_of_norm_tendsto_zero

added theorem padic_polynomial_dist

Modified data/padics/padic_integers.lean

modified theorem padic_int.add_def

added theorem padic_int.cast_pow

added def padic_int.cau_seq_lim

added theorem padic_int.cau_seq_lim_spec

modified theorem padic_int.coe_add

modified theorem padic_int.coe_mul

modified theorem padic_int.coe_one

modified theorem padic_int.coe_sub

added theorem padic_int.coe_zero

added theorem padic_int.complete

modified theorem padic_int.inv_mul

modified theorem padic_int.maximal_ideal_add

modified theorem padic_int.maximal_ideal_mul

modified theorem padic_int.maximal_ideal_ne_univ

modified theorem padic_int.mul_def

modified theorem padic_int.mul_inv

added theorem padic_int.tendsto_limit

modified theorem padic_int.zero_def

added theorem padic_norm_z.add_eq_max_of_ne

added theorem padic_norm_z.eq_of_norm_add_lt_left

added theorem padic_norm_z.eq_of_norm_add_lt_right

modified theorem padic_norm_z.le_one

modified theorem padic_norm_z.norm_one

added theorem padic_norm_z.one

added theorem padic_norm_z.padic_norm_e_of_padic_int

added theorem padic_norm_z.padic_norm_z_eq_padic_norm_e

added theorem padic_norm_z.padic_val_of_cong_pow_p

added theorem padic_norm_z.pow

Modified data/padics/padic_norm.lean

added theorem padic_norm.le_of_dvd

modified theorem padic_val.padic_val_eq_zero_of_coprime

added theorem padic_val.pow_dvd_iff_le_padic_val

added theorem padic_val.pow_dvd_of_le_padic_val

added theorem padic_val_rat.padic_val_rat_of_int

Renamed data/padics/padic_rationals.lean to data/padics/padic_numbers.lean

added def padic.cau_seq_lim

added theorem padic.cau_seq_lim_spec

modified theorem padic.complete'

added theorem padic.padic_norm_e_lim_le

added theorem padic.tendsto_limit

added theorem padic_norm_e.add_eq_max_of_ne'

added theorem padic_norm_e.add_eq_max_of_ne

modified theorem padic_norm_e.defn

added theorem padic_norm_e.eq_of_norm_add_lt_left

added theorem padic_norm_e.eq_of_norm_add_lt_right

added theorem padic_norm_e.norm_rat_le_one

added theorem padic_seq.add_eq_max_of_ne

added theorem padic_seq.lift_index_left

added theorem padic_seq.lift_index_left_left

added theorem padic_seq.lift_index_right

added theorem padic_seq.norm_eq_of_add_equiv_zero

modified theorem padic_seq.norm_nonarchimedean

Modified data/polynomial.lean

added def polynomial.binom_expansion

added theorem polynomial.continuous_eval

added theorem polynomial.derivative_eval

added def polynomial.eval_sub_factor

added theorem polynomial.eval_sum

added def polynomial.pow_add_expansion

added def polynomial.pow_sub_pow_factor

Modified data/rat.lean

added theorem rat.div_num_denom

added theorem rat.zero_iff_num_zero

Modified data/real/cau_seq.lean

Created data/real/cau_seq_filter.lean

added theorem cauchy_of_filter_cauchy

added theorem filter_cauchy_of_cauchy