module module

`IndisputableMonolith.Foundation.SpinStatistics`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import
IndisputableMonolith.Foundation.EightTick module_import

declarations in this module (12)

def IsFermionic L32
def IsBosonic L36
def rotationPhase L39
theorem fermion_rotation_phase_neg_one L43
theorem boson_rotation_phase_pos_one L49
theorem exchange_sign_fermion L58
theorem exchange_sign_boson L61
theorem spin_statistics_theorem L75
theorem pauli_exclusion L91
theorem pauli_exclusion_simple L99
theorem cpt_composition L107
theorem spin_statistics_certificate L117