The point group of a crystallographic group is finite

Proved

LeanEval.Geometry.SpaceGroupsProblem.pointGroupSet_finite_of_crystallographic

by Gabewhigham · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

crystallographygeometrygroup-theory

Let $G$ be a crystallographic group in dimension $d$ : a subgroup of the Euclidean motion group $E_d$ of $\mathbb{R}^d$ that is discrete (for every point $x$ and every $\varepsilon>0$ only finitely many $g\in G$ move $x$ by at most $\varepsilon$ ) and contains $d$ linearly independent translations. Its point group is the set of linear parts of its elements,

P(G)=\{\mathrm{lin}(g)\;:\;g\in G\}\subseteq O(d).

The theorem asserts that $P(G)$ is a finite set.

This is the first structural finiteness statement in the theory of space groups: a crystallographic group has only finitely many possible rotational/reflective parts, so it is an extension of a finite group by its lattice of translations. It is the step that makes a classification of crystallographic groups into finitely many types conceivable.

Preamble

import Mathlib
import Definitions.Def_LeanEval_SpaceGroups_Definitions
import Definitions.Def_SpaceGroupsPointGroupDefs

Formal statement

namespace LeanEval
namespace Geometry
namespace SpaceGroupsProblem

theorem pointGroupSet_finite_of_crystallographic {d : ℕ} {G : Subgroup (EuclideanIsom d)}
    (hG : IsCrystallographicGroup G) : (pointGroupSet G).Finite := by sorry

end SpaceGroupsProblem
end Geometry
end LeanEval

Source

L. S. Charlap, Bieberbach Groups and Flat Manifolds, Springer 1986, Chapter I, Theorem 1.2 (the point group of a crystallographic group is finite).

View graph