mathlib

9d3c05ad - feat(ring_theory/simple_module): simple modules and Schur's Lemma (#5473)

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