OAI/RingTheory/Multiplicity/LocalContractibility.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.baseChangeLocalizationIso line 13
2. instance OAI.Lech.baseChangeLocalization_preservesFiniteLimits line 37
3. instance OAI.Lech.baseChangeLocalization_preservesFiniteColimits line 41
4. def OAI.Lech.localizationHomologyIso line 45
5. lemma OAI.Lech.localizationHomology_subsingleton_iff line 50
6. lemma OAI.Lech.acyclic_of_contractible line 60
7. def OAI.Lech.ContractibleOff line 74
8. lemma OAI.Lech.ContractibleOff.acyclicAway line 78
9. def OAI.Lech.LocallyContractibleOff line 97
10. lemma OAI.Lech.LocallyContractibleOff.acyclicAway line 101