Commit 2023-06-10 14:18 0b889932

View on Github →

feat: port CategoryTheory.Preadditive.Schur (#4952)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/Schur.lean

added theorem CategoryTheory.endomorphism_simple_eq_smul_id

added theorem CategoryTheory.finrank_endomorphism_eq_one

added theorem CategoryTheory.finrank_endomorphism_simple_eq_one

added theorem CategoryTheory.finrank_hom_simple_simple

added theorem CategoryTheory.finrank_hom_simple_simple_eq_one_iff

added theorem CategoryTheory.finrank_hom_simple_simple_eq_zero_iff

added theorem CategoryTheory.finrank_hom_simple_simple_eq_zero_of_not_iso

added theorem CategoryTheory.finrank_hom_simple_simple_le_one

added theorem CategoryTheory.isIso_iff_nonzero

added theorem CategoryTheory.isIso_of_hom_simple

added theorem CategoryTheory.mono_of_nonzero_from_simple