pith. machine review for the scientific record. sign in
inductive definition def or abbrev

Q3Element

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)

  56inductive Q3Element
  57  | pos_one  : Q3Element  -- +1
  58  | neg_one  : Q3Element  -- -1
  59  | pos_i    : Q3Element  -- +i
  60  | neg_i    : Q3Element  -- -i
  61  | pos_j    : Q3Element  -- +j
  62  | neg_j    : Q3Element  -- -j
  63  | pos_k    : Q3Element  -- +k
  64  | neg_k    : Q3Element  -- -k
  65  deriving DecidableEq, Repr
  66
  67/-- The spin-0 sector (scalar sector): {+1, -1}. These are the Higgs generators. -/

used by (2)

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