OAI/RingTheory/Multiplicity/PureProjective.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.PureProjective.sectionCycles line 12
2. lemma OAI.Lech.PureProjective.sectionCycles_π line 15
3. def OAI.Lech.PureProjective.inclusion line 18
4. lemma OAI.Lech.PureProjective.cycles_inclusion line 22
5. lemma OAI.Lech.PureProjective.homology_inclusion line 27
6. lemma OAI.Lech.PureProjective.inclusion_quasiIso line 33
7. def OAI.Lech.PureProjective.homotopyEquiv line 47