IndisputableMonolith.Algebra.F2Power

declarations in this module (28)

• def F2Power L49
• theorem zero_apply L67
• theorem add_apply L72
• theorem neg_eq_self L78
• theorem sub_eq_add L83
• theorem add_self L113
• theorem card_eq L121
• theorem nonzero_card L126
• theorem nonzero_card_three L140
• def hammingWeight L152
• theorem hammingWeight_zero L155
• theorem hammingWeight_le L159
• theorem weight_zero_iff L165
• theorem card_weight_zero_three L191
• def axis1 L203
• def axis2 L204
• def axis3 L205
• theorem axis1_weight L207
• theorem axis2_weight L211
• theorem axis3_weight L215
• def axis12 L220
• def axis13 L221
• def axis23 L222
• def axis123 L225
• theorem axis123_weight L227
• def oneDimSubspace L241
• theorem oneDimSubspace_card L244
• theorem oneDimSubspace_closed L250