theorem proved term proof

`D3_has_spinor_structure`

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

formal statement (Lean)

 223theorem D3_has_spinor_structure : HasRSSpinorStructure 3 := {

proof body

Term-mode proof.

 224  two_component := Or.inr rfl
 225  nonabelian := le_refl 3
 226  simple := Or.inl rfl
 227}
 228
 229/-- D = 1 does not have RS spinor structure (too few dimensions). -/

depends on (2)

Lean names referenced from this declaration's body.

le_refl in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
HasRSSpinorStructure in IndisputableMonolith.Foundation.DimensionForcing decl_use