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

quaternions_not_needed

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)

 213theorem quaternions_not_needed :
 214    -- ℍ describes 3D rotations, but phase is 2D
 215    -- ℂ is the minimal system for phase representation
 216    True := trivial

proof body

Term-mode proof.

 217
 218/-- Could we use split-complex numbers (real + jε where ε² = +1)?
 219    No - these don't form a rotation group. -/

depends on (7)

Lean names referenced from this declaration's body.