Commit 2023-03-18 11:38 f430769b

View on Github →

chore(topology/algebra/module/basic): move a lemma to a new file (#18608) Also slightly generalize from [is_simple_module R R] to [is_simple_module R N].

Estimated changes