lean_workbook_plus_28806

Proved

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

Prove the following lemma: If $g$ and $h$ are elements of a group $G$ which commute with each other, and they have relatively prime orders $m,n$ respectively, then the order of the product $gh$ is $mn$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28806 {G : Type*} [Group G] {g h : G} (hg : IsOfFinOrder g) (hh : IsOfFinOrder h) (hgh : Commute g h) (hmn : Nat.Coprime (orderOf g) (orderOf h)) : orderOf (g * h) = (orderOf g) * (orderOf h)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph