add_self

formal source

 110  zsmul := zsmulRec
 111  sub_eq_add_neg u v := by funext i; rfl
 112
 113@[simp] theorem add_self (v : F2Power D) : v + v = 0 := by
 114  funext i
 115  show xor (v i) (v i) = false
 116  cases v i <;> rfl
 117
 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