Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-25 10:09 e90c7b96

View on Github →

feat(data/num/prime): kernel-friendly decision procedure for prime (#3525)

Estimated changes

Modified src/algebra/ring/basic.lean

modified theorem dvd_iff_dvd_of_dvd_sub

modified theorem dvd_mul_sub_mul

added theorem two_dvd_bit0

added theorem two_dvd_bit1

Modified src/data/nat/basic.lean

Modified src/data/num/lemmas.lean

added theorem pos_num.dvd_to_nat

Created src/data/num/prime.lean

added def num.min_fac

added theorem num.min_fac_to_nat

added def num.prime

added def pos_num.min_fac

added def pos_num.min_fac_aux

added theorem pos_num.min_fac_aux_to_nat

added theorem pos_num.min_fac_to_nat

added def pos_num.prime