Order_of_Group_Element_in_Group_Direct_Product
Proveddirect-productgroup-theoryorderproofwiki
In the direct product G × H, the order of (g, h) is lcm(order(g), order(h)).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Order_of_Group_Element_in_Group_Direct_Product {G H : Type _} [Group G] [Group H] (g : G) (h : H) : orderOf (g, h) = Nat.lcm (orderOf g) (orderOf h) := by sorrySource