Theorem CategoryTheory.mono_iff_forall_injective

Modification history

2025-12-23 14:13
Mathlib/CategoryTheory/Category/Basic.lean
feat(CategoryTheory/Category/Basic): use `to_dual` (#33146) …
Deleted CategoryTheory.mono_iff_forall_injectiveView on Github →
2025-08-31 11:17
Mathlib/CategoryTheory/Category/Basic.lean
feat(CategoryTheory/Adjunction): lemmas on adjoint quadruples (#27720) …
Added CategoryTheory.mono_iff_forall_injectiveView on Github →