lean_workbook_plus_76520

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that in a finite abelian group $G$ , there exists an element $g$ whose order divides the order of every element in $G$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_76520 (G : Type*) [CommGroup G] [Finite G] : 
  ∃ g : G, ∀ h : G, orderOf g ∣ orderOf h   :=  by sorry

Source