Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-27 23:51 460df5ef

View on Github →

feat(tactic/norm_num): add support for primality proving

Estimated changes

Modified data/nat/gcd.lean

added theorem nat.exists_coprime'

modified theorem nat.exists_eq_prod_and_dvd_and_dvd

Modified data/nat/prime.lean

modified theorem nat.min_fac_eq

modified theorem nat.min_fac_le_of_dvd

added theorem nat.not_prime_mul

Modified tactic/norm_num.lean

added theorem norm_num.is_prime_helper

added theorem norm_num.min_fac_bit0

added theorem norm_num.min_fac_helper.n_pos

added def norm_num.min_fac_helper

added theorem norm_num.min_fac_helper_0

added theorem norm_num.min_fac_helper_1

added theorem norm_num.min_fac_helper_2

added theorem norm_num.min_fac_helper_3

added theorem norm_num.min_fac_helper_4

added theorem norm_num.min_fac_helper_5

added theorem norm_num.min_fac_ne_bit0

added theorem norm_num.not_prime_helper

Modified tactic/ring.lean