pith. machine review for the scientific record. sign in
theorem proved term proof

D1_no_spinor_structure

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)

 230theorem D1_no_spinor_structure : ¬HasRSSpinorStructure 1 := by

proof body

Term-mode proof.

 231  intro ⟨_, hna, _⟩
 232  norm_num at hna
 233
 234/-- D = 2 does not have RS spinor structure (abelian rotations). -/

depends on (1)

Lean names referenced from this declaration's body.