basic): move a lemma to a new file (#18608)

Commit

2 years ago

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]`.

Author

urkud

Parents

027ff1e4

mathlib f430769b - chore(topology/algebra/module/basic): move a lemma to a new file (#18608)

mathlib
f430769b - chore(topology/algebra/module/basic): move a lemma to a new file (#18608)