Theorem ComplexShape.Embedding.r_eq_none

Modification history

2024-06-24 07:53
Mathlib/Algebra/Homology/Embedding/Basic.lean
feat: the extension of a homological complex by an embedding of complex shapes (#13992)
Added ComplexShape.Embedding.r_eq_noneView on Github →