mathlib3

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

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. Co-authored-by: Oliver Nash <github@olivernash.org>