OAI/Analysis/JiangSu/DimensionDrop/DimensionDropGeneratedHom.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionDropRelations.Witness.generatedHom line 21
  2. lemma OAI.DimensionDropRelations.Witness.generatedHom_gen line 23
  3. def OAI.DimensionDropModel.indexEquiv line 39
  4. def OAI.DimensionDropModel.twistAmbient line 41
  5. lemma OAI.DimensionDropModel.reindex_left line 45
  6. lemma OAI.DimensionDropModel.reindex_right line 48
  7. lemma OAI.DimensionDropModel.twist_left line 59
  8. lemma OAI.DimensionDropModel.twist_right line 67
  9. def OAI.DimensionDropModel.concreteToGenerated line 74
  10. def OAI.DimensionDropRelations.Witness.dimensionDropHom line 93
  11. theorem OAI.DirectComparison.comparison_dimension_drop_hom line 111
  12. theorem OAI.JiangSuConstruction.consecutive_multiplicities line 136
  13. theorem OAI.JiangSuConstruction.prime_drop_into_consecutive line 160
  14. theorem OAI.DirectComparison.comparison_prime_drop_hom line 180