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

Commit

3 years ago

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 <scott.morrison@gmail.com>

Author

kim-em

Parents

e5b48f9b

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

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