card_eq

formal source

 118/-! ## Cardinality -/
 119
 120/-- `F2Power D` has `2 ^ D` elements. -/
 121theorem card_eq : Fintype.card (F2Power D) = 2 ^ D := by
 122  unfold F2Power
 123  simp [Fintype.card_bool, Fintype.card_fin]
 124
 125/-- The number of non-zero vectors in `F2Power D` is `2 ^ D - 1`. -/
 126theorem nonzero_card :
 127    (Finset.univ.filter (fun v : F2Power D => v ≠ 0)).card = 2 ^ D - 1 := by
 128  have h : (Finset.univ.filter (fun v : F2Power D => v ≠ 0)).card =
 129           Fintype.card (F2Power D) - 1 := by
 130    rw [show (Finset.univ.filter (fun v : F2Power D => v ≠ 0)) =
 131            Finset.univ.erase 0 from ?_, Finset.card_erase_of_mem (Finset.mem_univ _)]
 132    · rfl
 133    · ext v
 134      simp [Finset.mem_filter, Finset.mem_erase, Finset.mem_univ]
 135  rw [h, card_eq]
 136
 137/-- At `D = 3`, the non-zero count is `7`. The seven Booker plot
 138    families bijection in `Aesthetics.NarrativeGeodesic` chains off
 139    this corollary. -/
 140theorem nonzero_card_three :
 141    (Finset.univ.filter (fun v : F2Power 3 => v ≠ 0)).card = 7 := by
 142  have h := @nonzero_card 3
 143  -- h : … = 2 ^ 3 - 1
 144  have h2 : (2 : ℕ) ^ 3 - 1 = 7 := by norm_num
 145  rw [h2] at h
 146  exact h
 147
 148/-! ## Hamming weight -/
 149
 150/-- The Hamming weight of `v`: the number of coordinates equal to
 151    `true`. -/