theorem
proved
term proof
spin0_count
show as:
view Lean formalization →
formal statement (Lean)
77theorem spin0_count : Spin0Sector.length = 2 := by decide
proof body
Term-mode proof.
78
79/-- The spin-1 sector has 6 elements. -/