feat(category_theory/preadditive): End X is a division_ring or field when X is simple (#13849)
feat(category_theory/preadditive): End X is a division_ring or field when X is simple (#13849)

Consequences of Schur's lemma





Co-authored-by: Scott Morrison <63f04b4d96235eb042cc46d94f14d241d2a26722@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib