`axis2_weight`

proved

show as: view math explainer →

module: IndisputableMonolith.Algebra.F2Power
domain: Algebra
line: 211 · 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 211.

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

 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]
 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) :=

papers checked against this theorem

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