Commit 2025-12-09 03:43 ef704c53

feat(GroupTheory/OrderOfElement): Pi.orderOf_eq and its related and depended-upon theorems related to Pi, minimalPeriod, and IsPeriodicPt (#29204) The need for Pi.orderOf_eq comes in helping prove the value of the order of a ZMod number when used with ZMod.prodEquivPi. At first I was only trying to prove (a : (i : Fin n) → α i) : orderOf a = Finset.univ.lcm (fun i => orderOf (a i)), but after seeing the "Corresponding pi lemmas" comment, I realized that this could be generalized to Pi-types (Pi) and also some related and dependent theorems are not implemented yet, so I went on to add and prove these referring to those similar ones for product types (Prod).