Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-17 15:38 0acdf1cc

View on Github →

feat(data/nat): better sqrt + pairing, prime numbers, renames...

Estimated changes

Modified algebra/functions.lean

added theorem lt_min_iff

added theorem max_lt_iff

Modified algebra/group_power.lean

Modified algebra/order.lean

added theorem eq_or_lt_of_le

added theorem lt_iff_le_and_ne

Modified algebra/ring.lean

added theorem mul_dvd_mul_iff_left

added theorem mul_dvd_mul_iff_right

Modified data/finset/basic.lean

Modified data/int/basic.lean

Modified data/nat/basic.lean

added theorem nat.bit0_le_bit

added theorem nat.bit_le

added theorem nat.bit_le_bit1

added theorem nat.bit_lt_bit0

added theorem nat.bit_lt_bit

added theorem nat.bit_ne_zero

added theorem nat.dvd_fact

added def nat.fact

added theorem nat.fact_dvd_fact

added theorem nat.fact_le

added theorem nat.fact_ne_zero

added theorem nat.fact_one

added theorem nat.fact_pos

added theorem nat.fact_succ

added theorem nat.fact_zero

modified theorem nat.le_add_one_iff

modified theorem nat.le_zero_iff

added theorem nat.lt_pred_of_succ_lt

added theorem nat.lt_size

added theorem nat.lt_size_self

added theorem nat.lt_succ_iff

deleted theorem nat.lt_succ_iff_le

added theorem nat.lt_succ_iff_lt_or_eq

added theorem nat.mul_self_inj

added theorem nat.pos_iff_ne_zero'

added theorem nat.pos_iff_ne_zero

added theorem nat.pow_add

added theorem nat.pow_dvd_pow

added theorem nat.shiftl'_ne_zero_left

added theorem nat.shiftl'_tt_ne_zero

added theorem nat.size_bit0

added theorem nat.size_bit1

added theorem nat.size_bit

added theorem nat.size_eq_zero

added theorem nat.size_le

added theorem nat.size_le_size

added theorem nat.size_pos

added theorem nat.size_pow

added theorem nat.size_shiftl'

added theorem nat.size_shiftl

added theorem nat.size_zero

added theorem nat.sub_le_left_iff_le_add

added theorem nat.sub_le_right_iff_le_add

modified theorem nat.succ_le_succ_iff

Deleted data/nat/bquant.lean

deleted def ball'

deleted def ball

deleted theorem ball_of_ball_succ'

deleted theorem ball_of_ball_succ

deleted theorem ball_succ_of_ball

deleted theorem ball_zero'

deleted theorem ball_zero

deleted theorem not_ball_of_not

deleted theorem not_ball_succ_of_not_ball

deleted def step_p

Renamed data/nat/sub.lean to data/nat/dist.lean

Modified data/nat/gcd.lean

added theorem nat.coprime.coprime_dvd_left

added theorem nat.coprime.coprime_dvd_right

added theorem nat.coprime.coprime_mul_left

added theorem nat.coprime.coprime_mul_left_right

added theorem nat.coprime.coprime_mul_right

added theorem nat.coprime.coprime_mul_right_right

added theorem nat.coprime.dvd_of_dvd_mul_left

added theorem nat.coprime.dvd_of_dvd_mul_right

added theorem nat.coprime.eq_one_of_dvd

added theorem nat.coprime.gcd_eq_one

added theorem nat.coprime.gcd_mul_left_cancel

added theorem nat.coprime.gcd_mul_left_cancel_right

added theorem nat.coprime.gcd_mul_right_cancel

added theorem nat.coprime.gcd_mul_right_cancel_right

added theorem nat.coprime.mul

added theorem nat.coprime.mul_right

added theorem nat.coprime.pow

added theorem nat.coprime.pow_left

added theorem nat.coprime.pow_right

added theorem nat.coprime.symm

deleted theorem nat.coprime_mul

deleted theorem nat.coprime_mul_right

deleted theorem nat.coprime_of_coprime_dvd_left

deleted theorem nat.coprime_of_coprime_dvd_right

deleted theorem nat.coprime_of_coprime_mul_left

deleted theorem nat.coprime_of_coprime_mul_left_right

deleted theorem nat.coprime_of_coprime_mul_right

deleted theorem nat.coprime_of_coprime_mul_right_right

deleted theorem nat.coprime_pow

deleted theorem nat.coprime_pow_left

deleted theorem nat.coprime_pow_right

deleted theorem nat.coprime_swap

deleted theorem nat.dvd_of_coprime_of_dvd_mul_left

deleted theorem nat.dvd_of_coprime_of_dvd_mul_right

added theorem nat.gcd_eq_left

deleted theorem nat.gcd_eq_one_of_coprime

added theorem nat.gcd_eq_right

deleted theorem nat.gcd_mul_left_cancel_of_coprime

deleted theorem nat.gcd_mul_left_cancel_of_coprime_right

deleted theorem nat.gcd_mul_right_cancel_of_coprime

deleted theorem nat.gcd_mul_right_cancel_of_coprime_right

Modified data/nat/pairing.lean

modified theorem nat.unpair_lt

modified theorem nat.unpair_lt_aux

Created data/nat/prime.lean

added theorem nat.coprime_or_dvd_of_prime

added theorem nat.coprime_pow_primes

added theorem nat.coprime_primes

added def nat.decidable_prime_1

added theorem nat.dvd_of_prime_of_dvd_pow

added theorem nat.dvd_prime

added theorem nat.dvd_prime_ge_two

added theorem nat.dvd_prime_pow

added theorem nat.exists_dvd_of_not_prime2

added theorem nat.exists_dvd_of_not_prime

added theorem nat.exists_infinite_primes

added theorem nat.exists_prime_and_dvd

added def nat.min_fac

added def nat.min_fac_aux

added theorem nat.min_fac_aux_has_prop

added theorem nat.min_fac_dvd

added theorem nat.min_fac_eq

added theorem nat.min_fac_has_prop

added theorem nat.min_fac_le

added theorem nat.min_fac_le_of_dvd

added theorem nat.min_fac_one

added theorem nat.min_fac_pos

added theorem nat.min_fac_prime

added theorem nat.min_fac_zero

added theorem nat.not_prime_iff_min_fac_lt

added theorem nat.not_prime_one

added theorem nat.not_prime_zero

added theorem nat.prime.coprime_iff_not_dvd

added theorem nat.prime.coprime_pow_of_not_dvd

added theorem nat.prime.dvd_iff_not_coprime

added theorem nat.prime.dvd_mul

added theorem nat.prime.ge_two

added theorem nat.prime.gt_one

added theorem nat.prime.not_dvd_mul

added theorem nat.prime.not_dvd_one

added theorem nat.prime.pos

added theorem nat.prime.pred_pos

added def nat.prime

added theorem nat.prime_def_le_sqrt

added theorem nat.prime_def_lt'

added theorem nat.prime_def_lt

added theorem nat.prime_def_min_fac

added theorem nat.prime_three

added theorem nat.prime_two

added theorem nat.succ_pred_prime

Modified data/nat/sqrt.lean

deleted theorem nat.eq_zero_of_sqrt_eq_zero

added theorem nat.le_sqrt

modified theorem nat.le_three_of_sqrt_eq_one

added theorem nat.lt_succ_sqrt

deleted theorem nat.mul_square_cancel

added def nat.sqrt

added theorem nat.sqrt_add_eq

added def nat.sqrt_aux

added theorem nat.sqrt_aux_0

added theorem nat.sqrt_aux_1

added theorem nat.sqrt_aux_2

added theorem nat.sqrt_aux_dec

modified theorem nat.sqrt_eq

added theorem nat.sqrt_eq_zero

added theorem nat.sqrt_le

added theorem nat.sqrt_le_add

added theorem nat.sqrt_le_self

added theorem nat.sqrt_le_sqrt

deleted theorem nat.sqrt_lower

modified theorem nat.sqrt_lt

added theorem nat.sqrt_lt_self

deleted theorem nat.sqrt_mono

deleted theorem nat.sqrt_mul_eq

added theorem nat.sqrt_pos

deleted theorem nat.sqrt_pos_of_pos

deleted theorem nat.sqrt_upper

Modified data/rat.lean

Modified logic/basic.lean

added theorem not.imp

Modified tactic/rcases.lean

Modified topology/measurable_space.lean

deleted theorem nat.lt_succ_iff

Modified topology/topological_structures.lean

deleted theorem lt_min_iff

deleted theorem max_lt_iff