`card_weight_zero_three`

proved

show as: view math explainer →

module: IndisputableMonolith.Algebra.F2Power
domain: Algebra
line: 191 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Algebra.F2Power on GitHub at line 191.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 188matches Booker's primary/compound/transcendent classification. -/
 189
 190/-- The unique weight-0 element: the zero vector. -/
 191theorem card_weight_zero_three :
 192    (Finset.univ.filter (fun v : F2Power 3 => hammingWeight v = 0)).card = 1 := by
 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)`. -/
 203def axis1 : F2Power 3 := ![true, false, false]
 204def axis2 : F2Power 3 := ![false, true, false]
 205def axis3 : F2Power 3 := ![false, false, true]
 206
 207theorem axis1_weight : hammingWeight axis1 = 1 := by
 208  unfold hammingWeight axis1
 209  decide
 210
 211theorem axis2_weight : hammingWeight axis2 = 1 := by
 212  unfold hammingWeight axis2
 213  decide
 214
 215theorem axis3_weight : hammingWeight axis3 = 1 := by
 216  unfold hammingWeight axis3
 217  decide
 218
 219/-- The three weight-2 vectors. -/
 220def axis12 : F2Power 3 := ![true, true, false]
 221def axis13 : F2Power 3 := ![true, false, true]

papers checked against this theorem

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