OAI/GroupTheory/Kervaire/SignedIncidence.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KervaireIncidenceCurrent.contDiff_diag line 41
  2. def OAI.KervaireIncidenceCurrent.swapBlocks line 48
  3. lemma OAI.KervaireIncidenceCurrent.pair_cancel line 54
  4. def OAI.KervaireIncidenceCurrent.pairedMap line 61
  5. def OAI.KervaireIncidenceCurrent.coreMap line 67
  6. lemma OAI.KervaireIncidenceCurrent.paired_elementary_core line 72
  7. lemma OAI.KervaireIncidenceCurrent.core_elementary_model line 95
  8. def OAI.KervaireIncidenceCurrent.rightMulMap line 111
  9. lemma OAI.KervaireIncidenceCurrent.elementary_rightMul line 117
  10. lemma OAI.KervaireIncidenceCurrent.model_homotopic_paired_mul line 130
  11. def OAI.KervaireIncidenceCurrent.includeFirst line 142
  12. lemma OAI.KervaireIncidenceCurrent.includeFirst_injective line 148
  13. lemma OAI.KervaireIncidenceCurrent.diag_mulVec_includeFirst line 153
  14. lemma OAI.KervaireIncidenceCurrent.rank_of_incidence line 160
  15. lemma OAI.KervaireIncidenceCurrent.exists_paired_fixed line 196
  16. abbrev OAI.KervaireSignPairing.positive line 212
  17. abbrev OAI.KervaireSignPairing.negative line 213
  18. lemma OAI.KervaireSignPairing.sign_count line 215
  19. def OAI.KervaireSignPairing.positiveEquiv line 229
  20. def OAI.KervaireSignPairing.signsEquiv line 234
  21. lemma OAI.KervaireSignPairing.signsEquiv_pos line 239
  22. lemma OAI.KervaireSignPairing.signsEquiv_neg line 243
  23. def OAI.KervaireSignPairing.coordinates line 247
  24. def OAI.KervaireSignPairing.repeatMatrix line 263
  25. def OAI.KervaireSignPairing.repeatMap line 265
  26. def OAI.KervaireSignPairing.signedMatrix line 281
  27. lemma OAI.KervaireSignPairing.coordinates_inl line 285
  28. lemma OAI.KervaireSignPairing.coordinates_middle line 288
  29. lemma OAI.KervaireSignPairing.coordinates_last line 291
  30. lemma OAI.KervaireSignPairing.signedMatrix_coordinates line 295