def definition def or abbrev

`Spin1Sector`

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

formal statement (Lean)

  71def Spin1Sector : List Q3Element :=

proof body

Definition body.

  72  [Q3Element.pos_i, Q3Element.neg_i,
  73   Q3Element.pos_j, Q3Element.neg_j,
  74   Q3Element.pos_k, Q3Element.neg_k]
  75
  76/-- The spin-0 sector has 2 elements. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

q3_order in IndisputableMonolith.StandardModel.Q3Representations decl_use
spin1_count in IndisputableMonolith.StandardModel.Q3Representations decl_use

depends on (2)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
Q3Element in IndisputableMonolith.StandardModel.Q3Representations decl_use