BimoduleAugmentationEpi.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.BimoduleTotal.augmentation_epi_f line 16
Source documentation
A quasi-isomorphism onto a stalk is surjective in each degree; this is proved from its homology map, not imposed on the resolution data.
```
theorem augmentation_epi_f (n : ℤ) : Epi (res.augmentation.f n) := by
…
```