Commit 2023-04-27 02:53 8b1ed96f

View on Github →

feat: port CategoryTheory.Simple (#3510)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Simple.lean

added theorem CategoryTheory.Biprod.isIso_inl_iff_isZero

added theorem CategoryTheory.Simple.iff_of_iso

added theorem CategoryTheory.Simple.not_isZero

added theorem CategoryTheory.Simple.of_iso

added theorem CategoryTheory.cokernel_zero_of_nonzero_to_simple

added theorem CategoryTheory.epi_from_simple_zero_of_not_iso

added theorem CategoryTheory.epi_of_nonzero_to_simple

added theorem CategoryTheory.id_nonzero

added theorem CategoryTheory.indecomposable_of_simple

added theorem CategoryTheory.isIso_of_epi_of_nonzero

added theorem CategoryTheory.isIso_of_mono_of_nonzero

added theorem CategoryTheory.kernel_zero_of_nonzero_from_simple

added theorem CategoryTheory.mono_to_simple_zero_of_not_iso

added theorem CategoryTheory.simple_iff_subobject_isSimpleOrder

added theorem CategoryTheory.simple_of_cosimple

added theorem CategoryTheory.simple_of_isSimpleOrder_subobject

added theorem CategoryTheory.subobject_simple_iff_isAtom

added theorem CategoryTheory.zero_not_simple