theorem proved term proof

`one_third_exchange_phase`

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

formal statement (Lean)

 169theorem one_third_exchange_phase :
 170    laughlin_exchange_phase 3 = Real.pi / 3 := by

Term-mode proof.

 171  unfold laughlin_exchange_phase
 172  norm_num
 173
 174end QHE
 175end Physics
 176end IndisputableMonolith

Lean names referenced from this declaration's body.

laughlin_exchange_phase in IndisputableMonolith.Physics.QuantumHallEffect decl_use