OAI/Combinatorics/ParityLifts/PureComponents.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ParityWL.RankedBagTree.induce line 15
  2. def OAI.ParityWL.PureLeftMaps line 48
  3. instance OAI.ParityWL.pureLeftMapsFintype line 51
  4. def OAI.ParityWL.ComponentMask line 55
  5. instance OAI.ParityWL.componentMaskFintype line 58
  6. abbrev OAI.ParityWL.MaskLeft line 62
  7. abbrev OAI.ParityWL.MaskRight line 63
  8. def OAI.ParityWL.ComponentMaps line 65
  9. instance OAI.ParityWL.componentMapsFintype line 69
  10. def OAI.ParityWL.assembleFunction line 74
  11. lemma OAI.ParityWL.assembleFunction_left line 79
  12. lemma OAI.ParityWL.assembleFunction_right line 83
  13. lemma OAI.ParityWL.assembleFunction_isLeft line 88
  14. def OAI.ParityWL.assemblePure line 96
  15. lemma OAI.ParityWL.assemblePure_injective line 112
  16. lemma OAI.ParityWL.sum_adj_same_side line 134
  17. def OAI.ParityWL.mapMask line 137
  18. def OAI.ParityWL.mapComponents line 141
  19. lemma OAI.ParityWL.assemble_mapComponents line 154
  20. def OAI.ParityWL.componentEquiv line 167
  21. lemma OAI.ParityWL.pureLeft_card line 172