OAI/RingTheory/Multiplicity/NormalizedLengthTrivialRelation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.NormalizedLength.trivialRelation_of_injective_flat_lift line 18
  2. lemma OAI.Lech.NormalizedLength.Tower.finite_collection_stage line 38
  3. lemma OAI.Lech.NormalizedLength.Tower.nontrivial_limit line 46
  4. lemma OAI.Lech.NormalizedLength.Tower.local_limit line 50
  5. lemma OAI.Lech.NormalizedLength.Tower.local_to_limit line 58
  6. lemma OAI.Lech.NormalizedLength.Tower.flat_limit line 76
  7. lemma OAI.Lech.NormalizedLength.Tower.faithfullyFlat_limit line 89
  8. lemma OAI.Lech.NormalizedLength.liftBaseChange_mk_injective line 103
  9. lemma OAI.Lech.NormalizedLength.length_span_baseChange line 114
  10. lemma OAI.Lech.NormalizedLength.span_baseChange_eq_top line 125
  11. lemma OAI.Lech.NormalizedLength.Tower.stage_baseChange line 136
  12. lemma OAI.Lech.NormalizedLength.Tower.length_baseChange line 158
  13. def OAI.Lech.NormalizedLength.Tower.presentedLengths line 186
  14. lemma OAI.Lech.NormalizedLength.Tower.stage_mem_presentedLengths line 190
  15. theorem OAI.Lech.NormalizedLength.Tower.length_eq_sInf_presented line 206
  16. lemma OAI.Lech.NormalizedLength.map_le_annihilator_baseChange line 225
  17. lemma OAI.Lech.NormalizedLength.le_annihilator_submodule line 239
  18. def OAI.Lech.NormalizedLength.Tower.torsionPresentedLengths line 259
  19. lemma OAI.Lech.NormalizedLength.Tower.stage_mem_torsionPresentedLengths line 264
  20. theorem OAI.Lech.NormalizedLength.Tower.length_eq_sInf_torsionPresented line 291
  21. def OAI.Lech.RootTower.regularTower line 314
  22. def OAI.Lech.RootTower.normalizedLength line 347
  23. lemma OAI.Lech.RootTower.normalizedLength_stage line 351
  24. def OAI.Lech.TensorTransport.reindex line 376
  25. lemma OAI.Lech.TensorTransport.reindex_tmul line 382
  26. lemma OAI.Lech.TensorTransport.twist_tower line 393
  27. lemma OAI.Lech.TensorTransport.twist_length line 404
  28. lemma OAI.Lech.TensorTransport.twist_finite line 412
  29. lemma OAI.Lech.RootTower.normalizedLength_rootBaseChange line 430