def
definition
axis1
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Algebra.F2Power on GitHub at line 203.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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]
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