Commit 2022-12-22 09:08 412b1515

feat(group_theory/order_of_element): a condition on o(x) and o(y) that implies o(xy)=o(y) (#17997)

• The main theorem is order_of_mul_eq_right_of_forall_prime_mul_dvd, which depends on order_of_dvd_lcm_mul, a variant of order_of_mul_dvd_lcm, and dvd_of_forall_prime_mul_dvd.
• Also add lemmas factorization_prime_le_iff_dvd and factorization_lcm that were used in another approach towards the same theorem.