Theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.mk_surjective

Modification history

2024-06-25 06:39
Mathlib/CategoryTheory/GuitartExact/Basic.lean
feat(CategoryTheory): constructor for right derivability structures (#12676) …
Added CategoryTheory.TwoSquare.StructuredArrowRightwards.mk_surjectiveView on Github →