theorem
proved
term proof
axis3_weight
show as:
view Lean formalization →
formal statement (Lean)
215theorem axis3_weight : hammingWeight axis3 = 1 := by
proof body
Term-mode proof.
216 unfold hammingWeight axis3
217 decide
218
219/-- The three weight-2 vectors. -/