Theorem CategoryTheory.IsGrothendieckAbelian.exists_isIso_of_functor_from_monoOver

Modification history

2025-02-17 13:55
Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean
feat(CategoryTheory): subobjects in Grothendieck abelian categories (#21986) …
Added CategoryTheory.IsGrothendieckAbelian.exists_isIso_of_functor_from_monoOverView on Github →