Commit 2023-01-23 18:46 8631e2d5

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 ≤.