lean_workbook_plus_60482

Proved

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

Let $a,b$ two elements of a group. If $a$ has order $n>1$ and $a^{n-1}b=ab^{n-1}$ prove that $ab=ba$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60482  {G : Type*} [Group G] {a b : G} {n : ℕ} (h : 1 < n) (h' : a ^ n = 1) (h'' : a ^ (n - 1) * b = b * a ^ (n - 1)) :
  a * b = b * a   :=  by sorry

Source

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

View graph