Commit 2021-01-02 10:18 9d3c05ad

feat(ring_theory/simple_module): simple modules and Schur's Lemma (#5473) Defines is_simple_module in terms of is_simple_lattice Proves Schur's Lemma Defines division ring structure on the endomorphism ring of a simple module