165theorem weight_zero_iff (v : F2Power D) : 166 hammingWeight v = 0 ↔ v = 0 := by
proof body
Tactic-mode proof.
167 constructor 168 · intro h 169 unfold hammingWeight at h 170 rw [Finset.card_eq_zero] at h 171 funext i 172 have hi : i ∉ Finset.univ.filter (fun j => v j = true) := by 173 rw [h]; exact Finset.notMem_empty _ 174 simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi 175 -- hi : ¬ v i = true 176 cases hv : v i 177 · rfl 178 · exact absurd hv hi 179 · intro h 180 subst h 181 exact hammingWeight_zero 182 183/-! ## Weight decomposition at `D = 3` 184 185The seven non-zero vectors of `F2Power 3` partition by Hamming 186weight into 3 weight-1 (single-axis), 3 weight-2 (two-axis), and 1 187weight-3 (all-axes) class. This is the `1+3+3+1` decomposition that 188matches Booker's primary/compound/transcendent classification. -/ 189 190/-- The unique weight-0 element: the zero vector. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.