lean_workbook_plus_27569

Proved

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

Explain why the sets $M_d = \{x \in G : |x| = d\}$ are disjoint for different divisors $d$ of $n$ , where $G$ is a group and $|x|$ denotes the order of element $x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27569 (G : Type*) [Group G] (n : ℕ) (M : ℕ → Set G) (hM : ∀ d : ℕ, M d = {x : G | orderOf x = d}) : ∀ d1 d2 : ℕ, d1 ≠ d2 → M d1 ∩ M d2 = ∅   :=  by sorry

Source

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

View graph