OAI/RingTheory/Multiplicity/CartierTowerDevissage.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.mono_cokernel_shortExact line 13
2. lemma OAI.Lech.total_map_mono line 18
3. lemma OAI.Lech.homology_target_property_of_zero line 22
4. lemma OAI.Lech.homology_source_property_of_zero line 29
5. lemma OAI.Lech.TotalGhost.towerPath_mono line 41
6. lemma OAI.Lech.TotalGhost.towerPath_cokernel_property line 50