Commit 2022-05-02 13:45 9d3db534
View on Github →feat(category_theory/preadditive): End X is a division_ring or field when X is simple (#13849) Consequences of Schur's lemma
feat(category_theory/preadditive): End X is a division_ring or field when X is simple (#13849) Consequences of Schur's lemma