OAI/GroupTheory/FiniteType/FiniteIndexRegular.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteIndexRegular.coords line 12
  2. lemma OAI.FiniteIndexRegular.coords_mul_section line 23
  3. def OAI.FiniteIndexRegular.embedLM line 26
  4. def OAI.FiniteIndexRegular.embed line 30
  5. def OAI.FiniteIndexRegular.eval line 49
  6. lemma OAI.FiniteIndexRegular.eval_mk line 54
  7. def OAI.FiniteIndexRegular.slice line 64
  8. lemma OAI.FiniteIndexRegular.slice_single line 68
  9. def OAI.FiniteIndexRegular.slices line 73
  10. lemma OAI.FiniteIndexRegular.factor_coemul line 77
  11. lemma OAI.FiniteIndexRegular.slice_map line 82
  12. lemma OAI.FiniteIndexRegular.slices_eval_mk line 93
  13. lemma OAI.FiniteIndexRegular.ind_mk_left line 102
  14. def OAI.FiniteIndexRegular.invLM line 110
  15. lemma OAI.FiniteIndexRegular.inv_eval_mk line 114
  16. lemma OAI.FiniteIndexRegular.sum_slices line 138
  17. lemma OAI.FiniteIndexRegular.eval_inv line 153
  18. lemma OAI.FiniteIndexRegular.inv_eval line 167
  19. def OAI.FiniteIndexRegular.indIso line 176
  20. theorem OAI.FiniteIndexRegular.product_vanishing line 185
  21. def OAI.RegularProductR.relabel line 200
  22. lemma OAI.RegularProductR.relabel_comm line 203
  23. def OAI.RegularProductR.homologyRelabel line 217
  24. lemma OAI.RegularProductR.vanishing_relabel line 222