OAI/Analysis/InterpolatedFactors/CornerIndex.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeGroupFactorMain.WeightedCornerIndex.SelfIndex line 8
  2. abbrev OAI.FreeGroupFactorMain.WeightedCornerIndex.PairIndex line 9
  3. abbrev OAI.FreeGroupFactorMain.WeightedCornerIndex.Index line 10
  4. inductive OAI.FreeGroupFactorMain.WeightedCornerIndex.Kind line 12
  5. def OAI.FreeGroupFactorMain.WeightedCornerIndex.Kind.valid line 20
  6. instance OAI.FreeGroupFactorMain.WeightedCornerIndex.Kind.(instance at line 25) line 25
  7. def OAI.FreeGroupFactorMain.WeightedCornerIndex.Kind.transpose line 27
  8. def OAI.FreeGroupFactorMain.WeightedCornerIndex.endpoints line 33
  9. def OAI.FreeGroupFactorMain.WeightedCornerIndex.description line 36
  10. def OAI.FreeGroupFactorMain.WeightedCornerIndex.indexOf line 44
  11. theorem OAI.FreeGroupFactorMain.WeightedCornerIndex.indexOf_description line 60
  12. theorem OAI.FreeGroupFactorMain.WeightedCornerIndex.description_injective line 68
  13. theorem OAI.FreeGroupFactorMain.WeightedCornerIndex.description_valid line 71
  14. theorem OAI.FreeGroupFactorMain.WeightedCornerIndex.description_indexOf line 79
  15. theorem OAI.FreeGroupFactorMain.WeightedCornerIndex.description_flip line 89
  16. def OAI.FreeGroupFactorMain.WeightedCornerIndex.reservoirCode line 98