OAI/RingTheory/Multiplicity/KoszulConeFunctor.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Lech.Koszul.coneFunctor_linear line 32
  2. instance OAI.Lech.Koszul.tensorFunctor_linear line 46
  3. instance OAI.Lech.Koszul.single_linear line 53
  4. lemma OAI.Lech.Koszul.scalar_homology_zero_of_factorization line 70
  5. lemma OAI.Lech.Koszul.scalar_smul_homology_zero_of_factorization line 82
  6. theorem OAI.Lech.PerfectDomainStages.normalizedLength_regular_koszul line 118
  7. theorem OAI.Lech.PerfectDomainStages.normalizedLength_coordinate_power_koszul line 160
  8. theorem OAI.Lech.PerfectDomainStages.normalizedLength_coordinate_koszul line 189
  9. def OAI.Lech.NormalizedLength.Tower.torsionLength line 245
  10. lemma OAI.Lech.Koszul.restrictScalars_map_scalar line 275
  11. def OAI.Lech.Koszul.restrictScalarsTensorIso line 286
  12. def OAI.Lech.Koszul.restrictScalarsHomologyIso line 299
  13. def OAI.Lech.Koszul.restrictScalarsTensorHomologyIso line 306
  14. def OAI.Lech.Koszul.restrictScalarsSingleTensorHomologyIso line 313
  15. def OAI.Lech.Koszul.coneTermEquiv line 331
  16. lemma OAI.Lech.Koszul.tensor_terms_free line 336
  17. lemma OAI.Lech.Koszul.tensor_terms_finite line 346
  18. lemma OAI.Lech.Koszul.unit_terms_free line 356
  19. lemma OAI.Lech.Koszul.unit_terms_finite line 367
  20. def OAI.Lech.Koszul.nullScalarIdeal line 379
  21. lemma OAI.Lech.Koszul.entryIdeal_le_nullScalarIdeal line 392
  22. lemma OAI.Lech.Koszul.unit_nullhomotopic_of_mem line 397
  23. theorem OAI.Lech.PerfectDomainStages.normalizedLength_parameter_koszul line 422