mathlib3
8631e2d5 - refactor(data/nat/parity): reduce imports, add/delete lemmas (#18221)

Commit
2 years ago
refactor(data/nat/parity): reduce imports, add/delete lemmas (#18221) Sync `mathlib3` with API changes introduced while porting `data.nat.parity` to Mathlib 4 in leanprover-community/mathlib4#1661. * Add `even.two_dvd`, `even.trans_dvd`, `has_dvd.dvd.even`, `odd.of_dvd_nat`, and `odd.ne_two_of_dvd_nat`. * Rename `nat.even_sub_one_of_prime_ne_two` to `nat.prime.even_sub_one`, move to `data.nat.prime`. * Delete `odd.factors_ne_two`. * Replace `is_primitive_root.pow_sub_one_norm_prime_pow_of_one_le` with `is_primitive_root.pow_sub_one_norm_prime_pow_of_ne_zero`, assume `≠ 0` instead of `1 ≤`.
Author
Parents
Loading