OAI/RingTheory/Multiplicity/ScalarChartComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.Homogeneous.awayCongr_restrict line 15
2. lemma OAI.Lech.FilteredFraction.chartEquiv_restrict line 29
3. def OAI.Lech.FilteredCech.diagram line 44
4. lemma OAI.Lech.FilteredCech.diagram_fullD line 58
5. def OAI.Lech.ReesRoot.scalarChartEquiv line 83
6. lemma OAI.Lech.ReesRoot.scalarChartEquiv_natural line 87
7. def OAI.Lech.ReesRoot.scalarSectionEquiv line 109
8. lemma OAI.Lech.ReesRoot.scalarSectionEquiv_natural line 120