OAI/RingTheory/Multiplicity/SignedCechBicRow.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.SignedCech.bicRowHomotopy line 27
  2. def OAI.Lech.SignedCech.twistIndex line 33
  3. lemma OAI.Lech.SignedCech.twistIndex_eq line 37
  4. lemma OAI.Lech.SignedCech.twistIndex_le line 43
  5. def OAI.Lech.SignedCech.twistStep line 47
  6. lemma OAI.Lech.SignedCech.twistPath line 51
  7. lemma OAI.Lech.SignedCech.positive_homologyMap_zero line 64
  8. lemma OAI.Lech.SignedCech.positive_homologyMap_zero_of_le line 97
  9. lemma OAI.Lech.SignedCech.exists_uniform_positive_nilpotence line 109
  10. lemma OAI.Lech.SignedFraction.order_mul_le line 131
  11. lemma OAI.Lech.SignedFraction.smul_mem_shift line 137
  12. def OAI.Lech.SignedFraction.multiply line 150
  13. lemma OAI.Lech.SignedFraction.inclusion_multiply line 156
  14. def OAI.Lech.ComplexLift.lift line 171
  15. lemma OAI.Lech.ComplexLift.lift_comp line 178
  16. lemma OAI.Lech.homologyMap_smul line 193
  17. lemma OAI.Lech.extendMap_smul line 210
  18. instance OAI.Lech.SignedCech.inclusion_f_mono line 228
  19. def OAI.Lech.SignedCech.cochainMultiply line 236
  20. lemma OAI.Lech.SignedCech.cochainMultiply_inclusion line 247
  21. def OAI.Lech.SignedCech.multiply line 255
  22. lemma OAI.Lech.SignedCech.multiply_inclusion line 260
  23. def OAI.Lech.SignedCech.positiveMultiply line 265
  24. lemma OAI.Lech.SignedCech.positiveMultiply_inclusion line 271
  25. lemma OAI.Lech.TensorTotal.Right.map_smul line 314
  26. lemma OAI.Lech.SignedCech.annihilator_of_positive_nilpotence line 340
  27. lemma OAI.Lech.SignedCech.exists_uniform_positive_annihilator line 357
  28. lemma OAI.Lech.SignedCech.positive_homology_powerTorsion line 368
  29. lemma OAI.Lech.SignedCech.complex_nat line 386
  30. lemma OAI.Lech.SignedCech.positive_nat line 391
  31. lemma OAI.Lech.FilteredCech.positive_homology_powerTorsion line 404
  32. lemma OAI.Lech.prop_tensor_free_single line 421
  33. theorem OAI.Lech.acyclicity_of_koszul line 436