mathlib

4ed0bcae - feat(algebra/category/Module/simple): 1d modules over k-algebras are simple (#14023)

feat(algebra/category/Module/simple): 1d modules over k-algebras are simple (#14023) It feels like this should just be a special case of some interesting more general statement, but I'm failing to think what that is. If you notice let me know. Otherwise it's a good fact in any case. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>