OAI/RingTheory/Multiplicity/FiniteComplexTopInclusion.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.FiniteComplex.topInclusion line 16
  2. instance OAI.Lech.FiniteComplex.topInclusion_mono line 22
  3. def OAI.Lech.FiniteComplex.dropTop line 32
  4. def OAI.Lech.FiniteComplex.topShortComplex line 34
  5. lemma OAI.Lech.FiniteComplex.topShortExact line 37
  6. lemma OAI.Lech.FiniteComplex.topShortExact_eval line 42
  7. lemma OAI.Lech.FiniteComplex.topInclusion_f_isIso line 46
  8. lemma OAI.Lech.FiniteComplex.dropTop_X_top line 51
  9. lemma OAI.Lech.FiniteComplex.dropTop_π_isIso line 55
  10. def OAI.Lech.FiniteComplex.dropTopXIso line 60
  11. def OAI.Lech.FiniteComplex.topSplitting line 65
  12. lemma OAI.Lech.FiniteComplex.isZero_of_X line 79
  13. theorem OAI.Lech.FiniteComplex.devissage line 85
  14. theorem OAI.Lech.FiniteComplex.homology_devissage line 121
  15. lemma OAI.Lech.FiniteComplex.homology_devissage_to line 142
  16. abbrev OAI.Lech.BicomplexTotal.Row line 164
  17. abbrev OAI.Lech.BicomplexTotal.Double line 165
  18. abbrev OAI.Lech.BicomplexTotal.functor line 166
  19. def OAI.Lech.BicomplexTotal.degreeMap line 169
  20. lemma OAI.Lech.BicomplexTotal.ι_degreeMap line 172
  21. lemma OAI.Lech.BicomplexTotal.degreeMap_id line 177
  22. lemma OAI.Lech.BicomplexTotal.degreeMap_comp line 182
  23. lemma OAI.Lech.BicomplexTotal.degreeMap_add line 192
  24. lemma OAI.Lech.BicomplexTotal.map_f line 200
  25. instance OAI.Lech.BicomplexTotal.(instance at line 205) line 205
  26. def OAI.Lech.BicomplexTotal.splitting line 213
  27. lemma OAI.Lech.BicomplexTotal.devissage line 233
  28. def OAI.Lech.powerTorsion line 253
  29. lemma OAI.Lech.powerTorsion_zero line 256
  30. lemma OAI.Lech.powerTorsion_mono line 261
  31. lemma OAI.Lech.powerTorsion_epi line 267
  32. lemma OAI.Lech.powerTorsion_extension line 273
  33. instance OAI.Lech.powerTorsion_serre line 289
  34. structure OAI.Lech.TorsionLength line 296
  35. lemma OAI.Lech.TorsionLength.le_of_mono line 305
  36. lemma OAI.Lech.TorsionLength.le_of_epi line 313
  37. def OAI.Lech.TorsionLength.zeroClass line 321
  38. def OAI.Lech.TorsionLength.finiteClass line 324
  39. instance OAI.Lech.TorsionLength.zeroClass_serre line 327
  40. instance OAI.Lech.TorsionLength.finiteClass_serre line 338
  41. lemma OAI.Lech.imageMap_isoModSerre line 357
  42. lemma OAI.Lech.TorsionLength.eq_of_iso line 379
  43. lemma OAI.Lech.TorsionLength.eq_of_isoModSerre line 383
  44. lemma OAI.Lech.TorsionLength.image_value_eq line 401
  45. lemma OAI.Lech.powerTorsion_prod line 417
  46. lemma OAI.Lech.powerTorsion_pi line 431
  47. lemma OAI.Lech.powerTorsion_fin line 442
  48. lemma OAI.Lech.TorsionLength.additive_linear line 456
  49. lemma OAI.Lech.TorsionLength.value_prod line 471
  50. lemma OAI.Lech.TorsionLength.value_linearEquiv line 490
  51. lemma OAI.Lech.TorsionLength.value_fin line 497
  52. lemma OAI.Lech.TorsionLength.value_fintype line 510