`OAI/Algebra/Finitistic/Ordinary/OrdinaryConeQuasiIso.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.quasiIso_iff_mappingCone_acyclic line 12
Source documentation
The actual native mapping cone detects quasi-isomorphisms.
```
theorem quasiIso_iff_mappingCone_acyclic : QuasiIso f ↔ (CochainComplex.mappingCone f).Acyclic := by
…
```