 222def axis23 : F2Power 3 := ![false, true, true]
 223
 224/-- The unique weight-3 vector. -/
 225def axis123 : F2Power 3 := ![true, true, true]
 226
 227theorem axis123_weight : hammingWeight axis123 = 3 := by
 228  unfold hammingWeight axis123
 229  decide
 230
 231/-! ## Subgroup count
 232
 233Every non-zero `v : F2Power D` generates the 1-dimensional subspace
 234`{0, v}` (closed under XOR because `v + v = 0`). The map
 235`v ↦ {0, v}` from non-zero vectors to 1-dimensional subspaces is a
 236bijection: every 1-dimensional `F2`-subspace consists of exactly two
 237elements (`0` and a single non-zero generator), and the generator is
 238unique. -/
 239
 240/-- The 1-dimensional subspace generated by a non-zero `v`. -/
 241def oneDimSubspace (v : F2Power D) : Finset (F2Power D) :=
 242  {0, v}
 243
 244theorem oneDimSubspace_card (v : F2Power D) (hv : v ≠ 0) :
 245    (oneDimSubspace v).card = 2 := by
 246  unfold oneDimSubspace
 247  simp [Finset.card_insert_of_notMem, Ne.symm hv]
 248
 249/-- The 1-dimensional subspace is closed under addition. -/
 250theorem oneDimSubspace_closed (v : F2Power D) (a b : F2Power D)
 251    (ha : a ∈ oneDimSubspace v) (hb : b ∈ oneDimSubspace v) :
 252    a + b ∈ oneDimSubspace v := by
 253  unfold oneDimSubspace at ha hb ⊢
 254  simp [Finset.mem_insert, Finset.mem_singleton] at ha hb ⊢
 255  rcases ha with ha | ha <;> rcases hb with hb | hb <;>

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.