theorem proved term proof

`int_or_half`

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)

  96theorem int_or_half (s : Spin) : s.isInteger ∨ s.isHalfInteger := by

proof body

Term-mode proof.

  97  unfold isInteger isHalfInteger
  98  omega
  99
 100/-- Integer and half-integer are mutually exclusive. -/

depends on (7)

Lean names referenced from this declaration's body.

and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
half in IndisputableMonolith.QFT.SpinStatistics decl_use
isHalfInteger in IndisputableMonolith.QFT.SpinStatistics decl_use
isInteger in IndisputableMonolith.QFT.SpinStatistics decl_use
Spin in IndisputableMonolith.QFT.SpinStatistics decl_use
half in IndisputableMonolith.RecogSpec.Core decl_use
half in IndisputableMonolith.Support.RungFractions decl_use