pith. machine review for the scientific record. sign in
theorem proved tactic proof

card_weight_zero_three

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)

 191theorem card_weight_zero_three :
 192    (Finset.univ.filter (fun v : F2Power 3 => hammingWeight v = 0)).card = 1 := by

proof body

Tactic-mode proof.

 193  have hsubset :
 194      (Finset.univ.filter (fun v : F2Power 3 => hammingWeight v = 0)) = {0} := by
 195    ext v
 196    simp [Finset.mem_filter, Finset.mem_univ, Finset.mem_singleton, weight_zero_iff]
 197  rw [hsubset]
 198  rfl
 199
 200/-- The three weight-1 vectors of `F2Power 3` are
 201    `(true, false, false)`, `(false, true, false)`,
 202    `(false, false, true)`. -/

depends on (8)

Lean names referenced from this declaration's body.