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)
80theorem spin1_count : Spin1Sector.length = 6 := by decide
proof body
Term-mode proof.
81
82/-- Q₃ has 8 elements total. -/
depends on (4)
Lean names referenced from this declaration's body.
-
has
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
total
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
total
in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget
decl_use
-
Spin1Sector
in IndisputableMonolith.StandardModel.Q3Representations
decl_use