Prove2Me

An explicit catalogue of the 230 space groups of R3\mathbb R^3

Definition
SpaceGroupCatalog

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

crystallographydiscrete-geometrygroup-theory

An explicit catalogue of one crystallographic group of R3\mathbb R^3 for each of the 230230 space-group types of the International Tables for Crystallography, Vol. A, written as concrete subgroups of the Euclidean motion group of E=R3E=\mathbb R^3 (the objects of the LeanEval definition bundle).

Lattice coordinates. Two lattice bases are used: the standard orthonormal basis (cubic), and hexagonal axes a1=(1,0,0)a_1=(1,0,0), a2=(−12,32,0)a_2=(-\tfrac12,\tfrac{\sqrt3}{2},0), a3=(0,0,1)a_3=(0,0,1) (hex). Coordinates u∈R3u\in\mathbb R^3 correspond to the point u1a1+u2a2+u3a3u_1a_1+u_2a_2+u_3a_3.

Symmetry operations. A symmetry operation is a pair (R,t)(R,t) of an integer 3×33\times3 matrix RR and an integer vector tt, standing for the affine map u↦Ru+t/12u\mapsto Ru+t/12 in lattice coordinates (every translation part occurring in the standard settings is a multiple of 1/121/12). Its Euclidean realisation SymOp.toIsom is the isometry gg of EE with g(u1a1+u2a2+u3a3)=∑i(Ru+t/12)i aig(u_1a_1+u_2a_2+u_3a_3)=\sum_i (Ru+t/12)_i\,a_i whenever such an isometry exists (it exists exactly when RR preserves the Gram matrix of the basis, which is the case for every operation used), and the identity otherwise.

The groups. A SpaceGroupData is a lattice basis together with a finite list of operations; its group SpaceGroupData.toSubgroup is the subgroup of the motion group generated by these operations together with the six lattice translations ±a1,±a2,±a3\pm a_1,\pm a_2,\pm a_3. The generators of type number nn were taken from the standard setting of ITA Vol. A (given by its Hall symbol: monoclinic groups with unique axis bb, cell choice 1; origin choice 1 where two origins are tabulated; rhombohedral groups on hexagonal axes); the generated group, modulo lattice translations, is exactly the full list of coordinate triplets of that setting. The second member of each of the 1111 enantiomorphic pairs (76,78)(76,78), (91,95)(91,95), (92,96)(92,96), (144,145)(144,145), (151,153)(151,153), (152,154)(152,154), (169,170)(169,170), (171,172)(171,172), (178,179)(178,179), (180,181)(180,181), (212,213)(212,213) is realised as the image of the first member under the point inversion x↦−xx\mapsto -x (SpaceGroupData.mirror, which replaces every (R,t)(R,t) by (R,−t)(R,-t)).

Index data. spaceGroupCatalog i is the group of type number i+1i+1. affineRepIndex lists the 219219 types other than the second members of the enantiomorphic pairs, affineClassIndex i is the position in that list of the representative of the affine class of type i+1i+1, enantiomorphicPairs lists the 1111 pairs, and sohnckeIndex lists the 6565 Sohncke types (all operations of positive determinant).

Definition code
import Mathlib
import Definitions.Def_LeanEval_SpaceGroups_Definitions

/-!
# An explicit catalogue of the 230 space-group types

For each of the 230 space-group types of the *International Tables for Crystallography*,
Vol. A, we record a concrete crystallographic subgroup of the Euclidean motion group of
`E 3 = EuclideanSpace ℝ (Fin 3)`.

A group is described in *lattice coordinates*.  A lattice kind fixes a basis
`a₁, a₂, a₃` of `E 3` (the columns of `LatticeKind.basisMatrix`):

* `cubic`: the standard orthonormal basis;
* `hex`: `a₁ = (1, 0, 0)`, `a₂ = (-1/2, √3/2, 0)`, `a₃ = (0, 0, 1)` (hexagonal axes).

A symmetry operation `⟨R, t⟩` (an integer matrix `R` and an integer vector `t`) stands for
the affine map which, in lattice coordinates, is `u ↦ R u + t / 12`.  All translation
parts of space-group operations in the standard settings are multiples of `1/12`.

The group attached to a `SpaceGroupData` is the subgroup generated by the listed operations
together with the six lattice translations `±a₁, ±a₂, ±a₃`.

The generators were taken from the standard (first) Hall setting of every type, i.e. the
setting tabulated in ITA Vol. A (monoclinic groups with unique axis `b`, cell choice 1;
origin choice 1 where two origins are tabulated; rhombohedral groups on hexagonal axes).
The second member of each of the 11 enantiomorphic pairs is realised as the image of the
first member under the point inversion `x ↦ -x` (`SpaceGroupData.mirror`).
-/

namespace LeanEval
namespace Geometry
namespace SpaceGroupsProblem
namespace SpaceGroupCatalog

/-- The two lattice bases used by the catalogue. -/
inductive LatticeKind where
  /-- the standard orthonormal basis of `ℝ³` -/
  | cubic
  /-- hexagonal axes `(1,0,0)`, `(-1/2,√3/2,0)`, `(0,0,1)` -/
  | hex
  deriving DecidableEq

/-- The basis matrix of a lattice kind: its columns are the lattice basis vectors. -/
noncomputable def LatticeKind.basisMatrix : LatticeKind → Matrix (Fin 3) (Fin 3) ℝ
  | .cubic => 1
  | .hex => !![1, -1 / 2, 0; 0, √3 / 2, 0; 0, 0, 1]

/-- Twice the Gram matrix of the lattice basis (an integer matrix). -/
def LatticeKind.gram2 : LatticeKind → Matrix (Fin 3) (Fin 3) ℤ
  | .cubic => !![2, 0, 0; 0, 2, 0; 0, 0, 2]
  | .hex => !![2, -1, 0; -1, 2, 0; 0, 0, 2]

/-- Lattice coordinates `u ↦ u₁ a₁ + u₂ a₂ + u₃ a₃ ∈ E 3`. -/
noncomputable def LatticeKind.coordMap (k : LatticeKind) : (Fin 3 → ℝ) →ₗ[ℝ] E 3 :=
  (WithLp.linearEquiv 2 ℝ (Fin 3 → ℝ)).symm.toLinearMap ∘ₗ Matrix.toLin' k.basisMatrix

/-- A symmetry operation in lattice coordinates: `u ↦ rot u + tr / 12`. -/
structure SymOp where
  /-- the linear part, an integer matrix in lattice coordinates -/
  rot : Matrix (Fin 3) (Fin 3) ℤ
  /-- the translation part, in units of `1/12` of the lattice basis vectors -/
  tr : Fin 3 → ℤ
  deriving DecidableEq

/-- The affine map of lattice coordinates `u ↦ rot u + tr / 12`. -/
noncomputable def SymOp.coordAction (o : SymOp) (u : Fin 3 → ℝ) : Fin 3 → ℝ :=
  Matrix.mulVec (o.rot.map (Int.cast : ℤ → ℝ)) u + fun i => (o.tr i : ℝ) / 12

open Classical in
/-- The Euclidean isometry described by a symmetry operation in the lattice basis `k`:
the isometry `g` with `g (coordMap u) = coordMap (rot u + tr / 12)` for all `u`, whenever
such an isometry exists (it does for every operation used in the catalogue), and the
identity otherwise. -/
noncomputable def SymOp.toIsom (k : LatticeKind) (o : SymOp) : EuclideanIsom 3 :=
  if h : ∃ g : EuclideanIsom 3, ∀ u : Fin 3 → ℝ, g (k.coordMap u) = k.coordMap (o.coordAction u)
  then h.choose else 1

/-- The mirror image of an operation under conjugation by the point inversion `x ↦ -x`. -/
def SymOp.mirror (o : SymOp) : SymOp := ⟨o.rot, -o.tr⟩

/-- The six lattice translations `±a₁, ±a₂, ±a₃` (translation parts in units of `1/12`). -/
def latticeOps : List SymOp :=
  [⟨1, ![12, 0, 0]⟩, ⟨1, ![0, 12, 0]⟩, ⟨1, ![0, 0, 12]⟩,
   ⟨1, ![-12, 0, 0]⟩, ⟨1, ![0, -12, 0]⟩, ⟨1, ![0, 0, -12]⟩]

/-- Data for one space group: a lattice basis and a list of generating operations. -/
structure SpaceGroupData where
  /-- the lattice basis in which the operations are written -/
  kind : LatticeKind
  /-- generating operations (besides the lattice translations) -/
  gens : List SymOp
  deriving DecidableEq

/-- The mirror image of a space group under the point inversion `x ↦ -x`. -/
def SpaceGroupData.mirror (D : SpaceGroupData) : SpaceGroupData :=
  ⟨D.kind, D.gens.map SymOp.mirror⟩

/-- The subgroup of `EuclideanIsom 3` generated by the operations of `D` together with the
lattice translations. -/
noncomputable def SpaceGroupData.toSubgroup (D : SpaceGroupData) : Subgroup (EuclideanIsom 3) :=
  Subgroup.closure {g | ∃ o ∈ latticeOps ++ D.gens, g = o.toIsom D.kind}

/-- No. 1 (`P1`, Hall symbol `P 1`). -/
def sg001 : SpaceGroupData := ⟨.cubic, []⟩

/-- No. 2 (`P-1`, Hall symbol `-P 1`). -/
def sg002 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 3 (`P2`, Hall symbol `P 2y`). -/
def sg003 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, 1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 4 (`P2_1`, Hall symbol `P 2yb`). -/
def sg004 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, 1, 0; 0, 0, -1], ![0, 6, 0]⟩]⟩

/-- No. 5 (`C2`, Hall symbol `C 2y`). -/
def sg005 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, 1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 6 (`Pm`, Hall symbol `P -2y`). -/
def sg006 : SpaceGroupData := ⟨.cubic, [⟨!![1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 7 (`Pc`, Hall symbol `P -2yc`). -/
def sg007 : SpaceGroupData := ⟨.cubic, [⟨!![1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 8 (`Cm`, Hall symbol `C -2y`). -/
def sg008 : SpaceGroupData := ⟨.cubic, [⟨!![1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 9 (`Cc`, Hall symbol `C -2yc`). -/
def sg009 : SpaceGroupData := ⟨.cubic, [⟨!![1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 10 (`P2/m`, Hall symbol `-P 2y`). -/
def sg010 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 11 (`P2_1/m`, Hall symbol `-P 2yb`). -/
def sg011 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, -1], ![0, 6, 0]⟩]⟩

/-- No. 12 (`C2/m`, Hall symbol `-C 2y`). -/
def sg012 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 13 (`P2/c`, Hall symbol `-P 2yc`). -/
def sg013 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, -1], ![0, 0, 6]⟩]⟩

/-- No. 14 (`P2_1/c`, Hall symbol `-P 2ybc`). -/
def sg014 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, -1], ![0, 6, 6]⟩]⟩

/-- No. 15 (`C2/c`, Hall symbol `-C 2yc`). -/
def sg015 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, -1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 16 (`P222`, Hall symbol `P 2 2`). -/
def sg016 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 17 (`P222_1`, Hall symbol `P 2c 2`). -/
def sg017 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 18 (`P2_12_12`, Hall symbol `P 2 2ab`). -/
def sg018 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 19 (`P2_12_12_1`, Hall symbol `P 2ac 2ab`). -/
def sg019 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 0, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 20 (`C222_1`, Hall symbol `C 2c 2`). -/
def sg020 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 21 (`C222`, Hall symbol `C 2 2`). -/
def sg021 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 22 (`F222`, Hall symbol `F 2 2`). -/
def sg022 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 6, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 0, 6]⟩]⟩

/-- No. 23 (`I222`, Hall symbol `I 2 2`). -/
def sg023 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 24 (`I2_12_12_1`, Hall symbol `I 2b 2c`). -/
def sg024 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 6, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 25 (`Pmm2`, Hall symbol `P 2 -2`). -/
def sg025 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 26 (`Pmc2_1`, Hall symbol `P 2c -2`). -/
def sg026 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 27 (`Pcc2`, Hall symbol `P 2 -2c`). -/
def sg027 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 28 (`Pma2`, Hall symbol `P 2 -2a`). -/
def sg028 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 0, 0]⟩]⟩

/-- No. 29 (`Pca2_1`, Hall symbol `P 2c -2ac`). -/
def sg029 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 0, 6]⟩]⟩

/-- No. 30 (`Pnc2`, Hall symbol `P 2 -2bc`). -/
def sg030 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 6, 6]⟩]⟩

/-- No. 31 (`Pmn2_1`, Hall symbol `P 2ac -2`). -/
def sg031 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 0, 6]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 32 (`Pba2`, Hall symbol `P 2 -2ab`). -/
def sg032 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 33 (`Pna2_1`, Hall symbol `P 2c -2n`). -/
def sg033 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 34 (`Pnn2`, Hall symbol `P 2 -2n`). -/
def sg034 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 35 (`Cmm2`, Hall symbol `C 2 -2`). -/
def sg035 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 36 (`Cmc2_1`, Hall symbol `C 2c -2`). -/
def sg036 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 37 (`Ccc2`, Hall symbol `C 2 -2c`). -/
def sg037 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 38 (`Amm2`, Hall symbol `A 2 -2`). -/
def sg038 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 6, 6]⟩]⟩

/-- No. 39 (`Aem2`, Hall symbol `A 2 -2b`). -/
def sg039 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 6, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 6, 6]⟩]⟩

/-- No. 40 (`Ama2`, Hall symbol `A 2 -2a`). -/
def sg040 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 6, 6]⟩]⟩

/-- No. 41 (`Aea2`, Hall symbol `A 2 -2ab`). -/
def sg041 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 6, 6]⟩]⟩

/-- No. 42 (`Fmm2`, Hall symbol `F 2 -2`). -/
def sg042 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 6, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 0, 6]⟩]⟩

/-- No. 43 (`Fdd2`, Hall symbol `F 2 -2d`). -/
def sg043 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![3, 9, 9]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 44 (`Imm2`, Hall symbol `I 2 -2`). -/
def sg044 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 45 (`Iba2`, Hall symbol `I 2 -2c`). -/
def sg045 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 46 (`Ima2`, Hall symbol `I 2 -2a`). -/
def sg046 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 47 (`Pmmm`, Hall symbol `-P 2 2`). -/
def sg047 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 48 (`Pnnn`, Hall symbol `P 2 2 -1n`). -/
def sg048 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 49 (`Pccm`, Hall symbol `-P 2 2c`). -/
def sg049 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 6]⟩]⟩

/-- No. 50 (`Pban`, Hall symbol `P 2 2 -1ab`). -/
def sg050 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 51 (`Pmma`, Hall symbol `-P 2a 2a`). -/
def sg051 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 0, 0]⟩]⟩

/-- No. 52 (`Pnna`, Hall symbol `-P 2a 2bc`). -/
def sg052 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 6, 6]⟩]⟩

/-- No. 53 (`Pmna`, Hall symbol `-P 2ac 2`). -/
def sg053 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 0, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 54 (`Pcca`, Hall symbol `-P 2a 2ac`). -/
def sg054 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 0, 6]⟩]⟩

/-- No. 55 (`Pbam`, Hall symbol `-P 2 2ab`). -/
def sg055 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 56 (`Pccn`, Hall symbol `-P 2ab 2ac`). -/
def sg056 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 6, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 0, 6]⟩]⟩

/-- No. 57 (`Pbcm`, Hall symbol `-P 2c 2b`). -/
def sg057 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 6, 0]⟩]⟩

/-- No. 58 (`Pnnm`, Hall symbol `-P 2 2n`). -/
def sg058 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 59 (`Pmmn`, Hall symbol `P 2 2ab -1ab`). -/
def sg059 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 60 (`Pbcn`, Hall symbol `-P 2n 2ab`). -/
def sg060 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 6, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 61 (`Pbca`, Hall symbol `-P 2ac 2ab`). -/
def sg061 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 0, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 62 (`Pnma`, Hall symbol `-P 2ac 2n`). -/
def sg062 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 0, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 63 (`Cmcm`, Hall symbol `-C 2c 2`). -/
def sg063 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 64 (`Cmce`, Hall symbol `-C 2ac 2`). -/
def sg064 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 0, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 65 (`Cmmm`, Hall symbol `-C 2 2`). -/
def sg065 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 66 (`Cccm`, Hall symbol `-C 2 2c`). -/
def sg066 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 67 (`Cmme`, Hall symbol `-C 2a 2`). -/
def sg067 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 68 (`Ccce`, Hall symbol `C 2 2 -1ac`). -/
def sg068 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 0, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 69 (`Fmmm`, Hall symbol `-F 2 2`). -/
def sg069 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 6, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 0, 6]⟩]⟩

/-- No. 70 (`Fddd`, Hall symbol `F 2 2 -1d`). -/
def sg070 : SpaceGroupData := ⟨.cubic, [⟨!![1, 0, 0; 0, 1, 0; 0, 0, -1], ![3, 3, 3]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 71 (`Immm`, Hall symbol `-I 2 2`). -/
def sg071 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 72 (`Ibam`, Hall symbol `-I 2 2c`). -/
def sg072 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 73 (`Ibca`, Hall symbol `-I 2b 2c`). -/
def sg073 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 6, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 74 (`Imma`, Hall symbol `-I 2b 2`). -/
def sg074 : SpaceGroupData := ⟨.cubic, [⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 6, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 75 (`P4`, Hall symbol `P 4`). -/
def sg075 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 76 (`P4_1`, Hall symbol `P 4w`). -/
def sg076 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 3]⟩]⟩

/-- No. 77 (`P4_2`, Hall symbol `P 4c`). -/
def sg077 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 78 (`P4_3`), realised as the mirror image of No. 76 under the point inversion `x ↦ -x`. -/
def sg078 : SpaceGroupData := sg076.mirror

/-- No. 79 (`I4`, Hall symbol `I 4`). -/
def sg079 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 80 (`I4_1`, Hall symbol `I 4bw`). -/
def sg080 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 6, 3]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 81 (`P-4`, Hall symbol `P -4`). -/
def sg081 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 82 (`I-4`, Hall symbol `I -4`). -/
def sg082 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 83 (`P4/m`, Hall symbol `-P 4`). -/
def sg083 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 84 (`P4_2/m`, Hall symbol `-P 4c`). -/
def sg084 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 85 (`P4/n`, Hall symbol `P 4ab -1ab`). -/
def sg085 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 86 (`P4_2/n`, Hall symbol `P 4n -1n`). -/
def sg086 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 87 (`I4/m`, Hall symbol `-I 4`). -/
def sg087 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 88 (`I4_1/a`, Hall symbol `I 4bw -1bw`). -/
def sg088 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 6, 3]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 6, 3]⟩]⟩

/-- No. 89 (`P422`, Hall symbol `P 4 2`). -/
def sg089 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 90 (`P42_12`, Hall symbol `P 4ab 2ab`). -/
def sg090 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 91 (`P4_122`, Hall symbol `P 4w 2c`). -/
def sg091 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 3]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 6]⟩]⟩

/-- No. 92 (`P4_12_12`, Hall symbol `P 4abw 2nw`). -/
def sg092 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 3]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 9]⟩]⟩

/-- No. 93 (`P4_222`, Hall symbol `P 4c 2`). -/
def sg093 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 94 (`P4_22_12`, Hall symbol `P 4n 2n`). -/
def sg094 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 95 (`P4_322`), realised as the mirror image of No. 91 under the point inversion `x ↦ -x`. -/
def sg095 : SpaceGroupData := sg091.mirror

/-- No. 96 (`P4_32_12`), realised as the mirror image of No. 92 under the point inversion `x ↦ -x`. -/
def sg096 : SpaceGroupData := sg092.mirror

/-- No. 97 (`I422`, Hall symbol `I 4 2`). -/
def sg097 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 98 (`I4_122`, Hall symbol `I 4bw 2bw`). -/
def sg098 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 6, 3]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 6, 3]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 99 (`P4mm`, Hall symbol `P 4 -2`). -/
def sg099 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 100 (`P4bm`, Hall symbol `P 4 -2ab`). -/
def sg100 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 101 (`P4_2cm`, Hall symbol `P 4c -2c`). -/
def sg101 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 102 (`P4_2nm`, Hall symbol `P 4n -2n`). -/
def sg102 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 6]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 103 (`P4cc`, Hall symbol `P 4 -2c`). -/
def sg103 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 104 (`P4nc`, Hall symbol `P 4 -2n`). -/
def sg104 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 105 (`P4_2mc`, Hall symbol `P 4c -2`). -/
def sg105 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 106 (`P4_2bc`, Hall symbol `P 4c -2ab`). -/
def sg106 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 107 (`I4mm`, Hall symbol `I 4 -2`). -/
def sg107 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 108 (`I4cm`, Hall symbol `I 4 -2c`). -/
def sg108 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 109 (`I4_1md`, Hall symbol `I 4bw -2`). -/
def sg109 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 6, 3]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 110 (`I4_1cd`, Hall symbol `I 4bw -2c`). -/
def sg110 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 6, 3]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 111 (`P-42m`, Hall symbol `P -4 2`). -/
def sg111 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 112 (`P-42c`, Hall symbol `P -4 2c`). -/
def sg112 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 6]⟩]⟩

/-- No. 113 (`P-42_1m`, Hall symbol `P -4 2ab`). -/
def sg113 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 114 (`P-42_1c`, Hall symbol `P -4 2n`). -/
def sg114 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 115 (`P-4m2`, Hall symbol `P -4 -2`). -/
def sg115 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 116 (`P-4c2`, Hall symbol `P -4 -2c`). -/
def sg116 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 117 (`P-4b2`, Hall symbol `P -4 -2ab`). -/
def sg117 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 0]⟩]⟩

/-- No. 118 (`P-4n2`, Hall symbol `P -4 -2n`). -/
def sg118 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 119 (`I-4m2`, Hall symbol `I -4 -2`). -/
def sg119 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 120 (`I-4c2`, Hall symbol `I -4 -2c`). -/
def sg120 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 121 (`I-42m`, Hall symbol `I -4 2`). -/
def sg121 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 122 (`I-42d`, Hall symbol `I -4 2bw`). -/
def sg122 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 6, 3]⟩]⟩

/-- No. 123 (`P4/mmm`, Hall symbol `-P 4 2`). -/
def sg123 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 124 (`P4/mcc`, Hall symbol `-P 4 2c`). -/
def sg124 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 6]⟩]⟩

/-- No. 125 (`P4/nbm`, Hall symbol `P 4 2 -1ab`). -/
def sg125 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 126 (`P4/nnc`, Hall symbol `P 4 2 -1n`). -/
def sg126 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 127 (`P4/mbm`, Hall symbol `-P 4 2ab`). -/
def sg127 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 128 (`P4/mnc`, Hall symbol `-P 4 2n`). -/
def sg128 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 129 (`P4/nmm`, Hall symbol `P 4ab 2ab -1ab`). -/
def sg129 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 130 (`P4/ncc`, Hall symbol `P 4ab 2n -1ab`). -/
def sg130 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 131 (`P4_2/mmc`, Hall symbol `-P 4c 2`). -/
def sg131 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 132 (`P4_2/mcm`, Hall symbol `-P 4c 2c`). -/
def sg132 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 6]⟩]⟩

/-- No. 133 (`P4_2/nbc`, Hall symbol `P 4n 2c -1n`). -/
def sg133 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 134 (`P4_2/nnm`, Hall symbol `P 4n 2 -1n`). -/
def sg134 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 135 (`P4_2/mbc`, Hall symbol `-P 4c 2ab`). -/
def sg135 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩]⟩

/-- No. 136 (`P4_2/mnm`, Hall symbol `-P 4n 2n`). -/
def sg136 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 137 (`P4_2/nmc`, Hall symbol `P 4n 2n -1n`). -/
def sg137 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 138 (`P4_2/ncm`, Hall symbol `P 4n 2ab -1n`). -/
def sg138 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 6]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 6, 6]⟩]⟩

/-- No. 139 (`I4/mmm`, Hall symbol `-I 4 2`). -/
def sg139 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 140 (`I4/mcm`, Hall symbol `-I 4 2c`). -/
def sg140 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 6]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 141 (`I4_1/amd`, Hall symbol `I 4bw 2bw -1bw`). -/
def sg141 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 6, 3]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 6, 3]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 6, 3]⟩]⟩

/-- No. 142 (`I4_1/acd`, Hall symbol `I 4bw 2aw -1bw`). -/
def sg142 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 6, 3]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 6, 3]⟩, ⟨!![1, 0, 0; 0, -1, 0; 0, 0, -1], ![6, 0, 3]⟩]⟩

/-- No. 143 (`P3`, Hall symbol `P 3`). -/
def sg143 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 144 (`P3_1`, Hall symbol `P 31`). -/
def sg144 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 4]⟩]⟩

/-- No. 145 (`P3_2`), realised as the mirror image of No. 144 under the point inversion `x ↦ -x`. -/
def sg145 : SpaceGroupData := sg144.mirror

/-- No. 146 (`R3`, Hall symbol `R 3`). -/
def sg146 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![8, 4, 4]⟩]⟩

/-- No. 147 (`P-3`, Hall symbol `-P 3`). -/
def sg147 : SpaceGroupData := ⟨.hex, [⟨!![0, 1, 0; -1, 1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 148 (`R-3`, Hall symbol `-R 3`). -/
def sg148 : SpaceGroupData := ⟨.hex, [⟨!![0, 1, 0; -1, 1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![8, 4, 4]⟩]⟩

/-- No. 149 (`P312`, Hall symbol `P 3 2`). -/
def sg149 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 150 (`P321`, Hall symbol `P 3 2"`). -/
def sg150 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 151 (`P3_112`, Hall symbol `P 31 2 (0 0 4)`). -/
def sg151 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 4]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 8]⟩]⟩

/-- No. 152 (`P3_121`, Hall symbol `P 31 2"`). -/
def sg152 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 4]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 153 (`P3_212`), realised as the mirror image of No. 151 under the point inversion `x ↦ -x`. -/
def sg153 : SpaceGroupData := sg151.mirror

/-- No. 154 (`P3_221`), realised as the mirror image of No. 152 under the point inversion `x ↦ -x`. -/
def sg154 : SpaceGroupData := sg152.mirror

/-- No. 155 (`R32`, Hall symbol `R 3 2"`). -/
def sg155 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![8, 4, 4]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 156 (`P3m1`, Hall symbol `P 3 -2"`). -/
def sg156 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 157 (`P31m`, Hall symbol `P 3 -2`). -/
def sg157 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 158 (`P3c1`, Hall symbol `P 3 -2"c`). -/
def sg158 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 159 (`P31c`, Hall symbol `P 3 -2c`). -/
def sg159 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 160 (`R3m`, Hall symbol `R 3 -2"`). -/
def sg160 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; -1, 0, 0; 0, 0, 1], ![8, 4, 4]⟩, ⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 161 (`R3c`, Hall symbol `R 3 -2"c`). -/
def sg161 : SpaceGroupData := ⟨.hex, [⟨!![0, -1, 0; -1, 0, 0; 0, 0, 1], ![8, 4, 10]⟩, ⟨!![0, -1, 0; 1, -1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 162 (`P-31m`, Hall symbol `-P 3 2`). -/
def sg162 : SpaceGroupData := ⟨.hex, [⟨!![0, 1, 0; -1, 1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 163 (`P-31c`, Hall symbol `-P 3 2c`). -/
def sg163 : SpaceGroupData := ⟨.hex, [⟨!![0, 1, 0; -1, 1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 6]⟩]⟩

/-- No. 164 (`P-3m1`, Hall symbol `-P 3 2"`). -/
def sg164 : SpaceGroupData := ⟨.hex, [⟨!![0, 1, 0; -1, 1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 165 (`P-3c1`, Hall symbol `-P 3 2"c`). -/
def sg165 : SpaceGroupData := ⟨.hex, [⟨!![0, 1, 0; -1, 1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, -1], ![0, 0, 6]⟩]⟩

/-- No. 166 (`R-3m`, Hall symbol `-R 3 2"`). -/
def sg166 : SpaceGroupData := ⟨.hex, [⟨!![0, 1, 0; -1, 1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, -1], ![8, 4, 4]⟩]⟩

/-- No. 167 (`R-3c`, Hall symbol `-R 3 2"c`). -/
def sg167 : SpaceGroupData := ⟨.hex, [⟨!![0, 1, 0; -1, 1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, -1], ![8, 4, 10]⟩]⟩

/-- No. 168 (`P6`, Hall symbol `P 6`). -/
def sg168 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 169 (`P6_1`, Hall symbol `P 61`). -/
def sg169 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 2]⟩]⟩

/-- No. 170 (`P6_5`), realised as the mirror image of No. 169 under the point inversion `x ↦ -x`. -/
def sg170 : SpaceGroupData := sg169.mirror

/-- No. 171 (`P6_2`, Hall symbol `P 62`). -/
def sg171 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 4]⟩]⟩

/-- No. 172 (`P6_4`), realised as the mirror image of No. 171 under the point inversion `x ↦ -x`. -/
def sg172 : SpaceGroupData := sg171.mirror

/-- No. 173 (`P6_3`, Hall symbol `P 6c`). -/
def sg173 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 174 (`P-6`, Hall symbol `P -6`). -/
def sg174 : SpaceGroupData := ⟨.hex, [⟨!![-1, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 175 (`P6/m`, Hall symbol `-P 6`). -/
def sg175 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 176 (`P6_3/m`, Hall symbol `-P 6c`). -/
def sg176 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 177 (`P622`, Hall symbol `P 6 2`). -/
def sg177 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 178 (`P6_122`, Hall symbol `P 61 2 (0 0 5)`). -/
def sg178 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 2]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 10]⟩]⟩

/-- No. 179 (`P6_522`), realised as the mirror image of No. 178 under the point inversion `x ↦ -x`. -/
def sg179 : SpaceGroupData := sg178.mirror

/-- No. 180 (`P6_222`, Hall symbol `P 62 2 (0 0 4)`). -/
def sg180 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 4]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 8]⟩]⟩

/-- No. 181 (`P6_422`), realised as the mirror image of No. 180 under the point inversion `x ↦ -x`. -/
def sg181 : SpaceGroupData := sg180.mirror

/-- No. 182 (`P6_322`, Hall symbol `P 6c 2c`). -/
def sg182 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 6]⟩]⟩

/-- No. 183 (`P6mm`, Hall symbol `P 6 -2`). -/
def sg183 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 184 (`P6cc`, Hall symbol `P 6 -2c`). -/
def sg184 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 185 (`P6_3cm`, Hall symbol `P 6c -2`). -/
def sg185 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 186 (`P6_3mc`, Hall symbol `P 6c -2c`). -/
def sg186 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 187 (`P-6m2`, Hall symbol `P -6 2`). -/
def sg187 : SpaceGroupData := ⟨.hex, [⟨!![-1, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 188 (`P-6c2`, Hall symbol `P -6c 2`). -/
def sg188 : SpaceGroupData := ⟨.hex, [⟨!![-1, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 6]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 189 (`P-62m`, Hall symbol `P -6 -2`). -/
def sg189 : SpaceGroupData := ⟨.hex, [⟨!![-1, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 190 (`P-62c`, Hall symbol `P -6c -2c`). -/
def sg190 : SpaceGroupData := ⟨.hex, [⟨!![-1, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 6]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩]⟩

/-- No. 191 (`P6/mmm`, Hall symbol `-P 6 2`). -/
def sg191 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 192 (`P6/mcc`, Hall symbol `-P 6 2c`). -/
def sg192 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 6]⟩]⟩

/-- No. 193 (`P6_3/mcm`, Hall symbol `-P 6c 2`). -/
def sg193 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 194 (`P6_3/mmc`, Hall symbol `-P 6c 2c`). -/
def sg194 : SpaceGroupData := ⟨.hex, [⟨!![1, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, -1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 6]⟩]⟩

/-- No. 195 (`P23`, Hall symbol `P 2 2 3`). -/
def sg195 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 196 (`F23`, Hall symbol `F 2 2 3`). -/
def sg196 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 6, 6]⟩]⟩

/-- No. 197 (`I23`, Hall symbol `I 2 2 3`). -/
def sg197 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![6, 6, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 198 (`P2_13`, Hall symbol `P 2ac 2ab 3`). -/
def sg198 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 0, 6]⟩]⟩

/-- No. 199 (`I2_13`, Hall symbol `I 2b 2c 3`). -/
def sg199 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, 1; -1, 0, 0; 0, -1, 0], ![0, 0, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 6, 0]⟩]⟩

/-- No. 200 (`Pm-3`, Hall symbol `-P 2 2 3`). -/
def sg200 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 201 (`Pn-3`, Hall symbol `P 2 2 3 -1n`). -/
def sg201 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![6, 6, 6]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 202 (`Fm-3`, Hall symbol `-F 2 2 3`). -/
def sg202 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![0, 6, 6]⟩]⟩

/-- No. 203 (`Fd-3`, Hall symbol `F 2 2 3 -1d`). -/
def sg203 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![3, 3, 3]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 204 (`Im-3`, Hall symbol `-I 2 2 3`). -/
def sg204 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 205 (`Pa-3`, Hall symbol `-P 2ac 2ab 3`). -/
def sg205 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![6, 0, 6]⟩]⟩

/-- No. 206 (`Ia-3`, Hall symbol `-I 2b 2c 3`). -/
def sg206 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![0, 0, 0]⟩, ⟨!![-1, 0, 0; 0, -1, 0; 0, 0, 1], ![0, 6, 0]⟩]⟩

/-- No. 207 (`P432`, Hall symbol `P 4 2 3`). -/
def sg207 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![0, 0, 0]⟩]⟩

/-- No. 208 (`P4_232`, Hall symbol `P 4n 2 3`). -/
def sg208 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 6]⟩, ⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![0, 0, 0]⟩]⟩

/-- No. 209 (`F432`, Hall symbol `F 4 2 3`). -/
def sg209 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![0, 6, 6]⟩]⟩

/-- No. 210 (`F4_132`, Hall symbol `F 4d 2 3`). -/
def sg210 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![3, 3, 3]⟩, ⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![0, 0, 0]⟩]⟩

/-- No. 211 (`I432`, Hall symbol `I 4 2 3`). -/
def sg211 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![6, 6, 6]⟩, ⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 212 (`P4_332`, Hall symbol `P 4acd 2ab 3`). -/
def sg212 : SpaceGroupData := ⟨.cubic, [⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![9, 3, 9]⟩, ⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![0, 0, 0]⟩]⟩

/-- No. 213 (`P4_132`), realised as the mirror image of No. 212 under the point inversion `x ↦ -x`. -/
def sg213 : SpaceGroupData := sg212.mirror

/-- No. 214 (`I4_132`, Hall symbol `I 4bd 2c 3`). -/
def sg214 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; 1, 0, 0; 0, -1, 0], ![6, 0, 0]⟩, ⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![3, 9, 3]⟩]⟩

/-- No. 215 (`P-43m`, Hall symbol `P -4 2 3`). -/
def sg215 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![0, 0, 0]⟩]⟩

/-- No. 216 (`F-43m`, Hall symbol `F -4 2 3`). -/
def sg216 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩, ⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![0, 6, 6]⟩]⟩

/-- No. 217 (`I-43m`, Hall symbol `I -4 2 3`). -/
def sg217 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![6, 6, 6]⟩, ⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![0, 0, 0]⟩]⟩

/-- No. 218 (`P-43n`, Hall symbol `P -4n 2 3`). -/
def sg218 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![6, 6, 6]⟩, ⟨!![0, 0, 1; 1, 0, 0; 0, 1, 0], ![0, 0, 0]⟩]⟩

/-- No. 219 (`F-43c`, Hall symbol `F -4a 2 3`). -/
def sg219 : SpaceGroupData := ⟨.cubic, [⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![6, 0, 0]⟩, ⟨!![0, -1, 0; 0, 0, -1; 1, 0, 0], ![0, 0, 0]⟩]⟩

/-- No. 220 (`I-43d`, Hall symbol `I -4bd 2c 3`). -/
def sg220 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, 1; -1, 0, 0; 0, -1, 0], ![0, 0, 6]⟩, ⟨!![0, 1, 0; -1, 0, 0; 0, 0, -1], ![3, 9, 3]⟩]⟩

/-- No. 221 (`Pm-3m`, Hall symbol `-P 4 2 3`). -/
def sg221 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![0, 0, 0]⟩, ⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 222 (`Pn-3n`, Hall symbol `P 4 2 3 -1n`). -/
def sg222 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![6, 6, 6]⟩, ⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩]⟩

/-- No. 223 (`Pm-3n`, Hall symbol `-P 4n 2 3`). -/
def sg223 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![0, 0, 0]⟩, ⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 224 (`Pn-3m`, Hall symbol `P 4n 2 3 -1n`). -/
def sg224 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![6, 6, 6]⟩, ⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 225 (`Fm-3m`, Hall symbol `-F 4 2 3`). -/
def sg225 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![0, 0, 0]⟩, ⟨!![0, 1, 0; -1, 0, 0; 0, 0, 1], ![0, 6, 6]⟩]⟩

/-- No. 226 (`Fm-3c`, Hall symbol `-F 4a 2 3`). -/
def sg226 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![0, 0, 0]⟩, ⟨!![0, 1, 0; 1, 0, 0; 0, 0, -1], ![0, 6, 0]⟩]⟩

/-- No. 227 (`Fd-3m`, Hall symbol `F 4d 2 3 -1d`). -/
def sg227 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![3, 3, 3]⟩, ⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![3, 3, 3]⟩]⟩

/-- No. 228 (`Fd-3c`, Hall symbol `F 4d 2 3 -1ad`). -/
def sg228 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![9, 3, 3]⟩, ⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![3, 3, 3]⟩]⟩

/-- No. 229 (`Im-3m`, Hall symbol `-I 4 2 3`). -/
def sg229 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![0, 0, 0]⟩, ⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![0, 0, 0]⟩, ⟨!![1, 0, 0; 0, 1, 0; 0, 0, 1], ![6, 6, 6]⟩]⟩

/-- No. 230 (`Ia-3d`, Hall symbol `-I 4bd 2c 3`). -/
def sg230 : SpaceGroupData := ⟨.cubic, [⟨!![0, 0, -1; -1, 0, 0; 0, -1, 0], ![0, 0, 0]⟩, ⟨!![0, -1, 0; 1, 0, 0; 0, 0, 1], ![3, 9, 3]⟩]⟩

/-- The data of the catalogue, indexed by ITA number minus one. -/
def catalogData : Fin 230 → SpaceGroupData := ![sg001, sg002, sg003, sg004, sg005, sg006, sg007, sg008, sg009, sg010, sg011, sg012, sg013, sg014, sg015, sg016, sg017, sg018, sg019, sg020, sg021, sg022, sg023, sg024, sg025, sg026, sg027, sg028, sg029, sg030, sg031, sg032, sg033, sg034, sg035, sg036, sg037, sg038, sg039, sg040, sg041, sg042, sg043, sg044, sg045, sg046, sg047, sg048, sg049, sg050, sg051, sg052, sg053, sg054, sg055, sg056, sg057, sg058, sg059, sg060, sg061, sg062, sg063, sg064, sg065, sg066, sg067, sg068, sg069, sg070, sg071, sg072, sg073, sg074, sg075, sg076, sg077, sg078, sg079, sg080, sg081, sg082, sg083, sg084, sg085, sg086, sg087, sg088, sg089, sg090, sg091, sg092, sg093, sg094, sg095, sg096, sg097, sg098, sg099, sg100, sg101, sg102, sg103, sg104, sg105, sg106, sg107, sg108, sg109, sg110, sg111, sg112, sg113, sg114, sg115, sg116, sg117, sg118, sg119, sg120, sg121, sg122, sg123, sg124, sg125, sg126, sg127, sg128, sg129, sg130, sg131, sg132, sg133, sg134, sg135, sg136, sg137, sg138, sg139, sg140, sg141, sg142, sg143, sg144, sg145, sg146, sg147, sg148, sg149, sg150, sg151, sg152, sg153, sg154, sg155, sg156, sg157, sg158, sg159, sg160, sg161, sg162, sg163, sg164, sg165, sg166, sg167, sg168, sg169, sg170, sg171, sg172, sg173, sg174, sg175, sg176, sg177, sg178, sg179, sg180, sg181, sg182, sg183, sg184, sg185, sg186, sg187, sg188, sg189, sg190, sg191, sg192, sg193, sg194, sg195, sg196, sg197, sg198, sg199, sg200, sg201, sg202, sg203, sg204, sg205, sg206, sg207, sg208, sg209, sg210, sg211, sg212, sg213, sg214, sg215, sg216, sg217, sg218, sg219, sg220, sg221, sg222, sg223, sg224, sg225, sg226, sg227, sg228, sg229, sg230]

/-- Indices (ITA number minus one) of the 219 representatives of the affine classes: all
types except the second member of each enantiomorphic pair
(78, 95, 96, 145, 153, 154, 170, 172, 179, 181, 213). -/
def affineRepIndex : Fin 219 → Fin 230 := ![0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 145, 146, 147, 148, 149, 150, 151, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 170, 172, 173, 174, 175, 176, 177, 179, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229]

/-- Indices (ITA number minus one) of the 65 Sohncke types, whose operations all preserve
orientation. -/
def sohnckeIndex : Fin 65 → Fin 230 := ![0, 2, 3, 4, 15, 16, 17, 18, 19, 20, 21, 22, 23, 74, 75, 76, 77, 78, 79, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 142, 143, 144, 145, 148, 149, 150, 151, 152, 153, 154, 167, 168, 169, 170, 171, 172, 176, 177, 178, 179, 180, 181, 194, 195, 196, 197, 198, 206, 207, 208, 209, 210, 211, 212, 213]

/-- For each index `i`, the position in `affineRepIndex` of the representative of the affine
class of type `i`: the type itself, or for the second member of an enantiomorphic pair, the
first member. -/
def affineClassIndex : Fin 230 → Fin 219 := ![0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 75, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 89, 90, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 140, 141, 142, 143, 144, 145, 146, 147, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 162, 163, 163, 164, 165, 166, 167, 168, 169, 169, 170, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218]

/-- The 11 enantiomorphic pairs, as pairs of indices (ITA number minus one):
(76, 78), (91, 95), (92, 96), (144, 145), (151, 153), (152, 154), (169, 170), (171, 172),
(178, 179), (180, 181), (212, 213). -/
def enantiomorphicPairs : List (Fin 230 × Fin 230) :=
  [(75, 77), (90, 94), (91, 95), (143, 144), (150, 152), (151, 153), (168, 169), (170, 171),
   (177, 178), (179, 180), (211, 212)]

/-- The catalogue: index `i` is the space-group type with ITA number `i + 1`. -/
noncomputable def spaceGroupCatalog (i : Fin 230) : Subgroup (EuclideanIsom 3) :=
  (catalogData i).toSubgroup

end SpaceGroupCatalog
end SpaceGroupsProblem
end Geometry
end LeanEval
Source
International Tables for Crystallography, Vol. A (T. Hahn, ed.), space-group tables 1–230 in their standard settings (via Hall symbols; S. R. Hall, Acta Cryst. A37 (1981) 517–525, and ITA Vol. B, Table A1.4.2.7). Enantiomorphic pairs and Sohncke types as in ITA Vol. A, Section 1.4 / Table 1.4.1 (230 types, 219 affine classes, 65 Sohncke types).

View graph