pith. machine review for the scientific record. sign in
structure definition def or abbrev

HasRSSpinorStructure

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 214structure HasRSSpinorStructure (D : Dimension) : Prop where
 215  /-- 2-component spinors -/
 216  two_component : spinorDimension D = 2 ∨ D = 3
 217  /-- Spin(D) is non-abelian — for D=3 this follows from Spin(3)≅SU(2) -/
 218  nonabelian : D ≥ 3
 219  /-- Spin(D) is simple (D = 3 or D ≥ 5) -/
 220  simple : D = 3 ∨ D ≥ 5
 221
 222/-- D = 3 has the RS spinor structure. -/

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.