mathlib3

d8de5672 - feat(group_theory/order_of_element): generalised to add_order_of (#6770)

feat(group_theory/order_of_element): generalised to add_order_of (#6770) This PR defines `add_order_of` for an additive monoid. If someone sees how to do this with more automation, let me know. This gets one step towards closing issue #1563. Coauthored by: Yakov Pechersky @pechersky Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>