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

Modified src/topology/algebra/module/basic.lean

deleted theorem linear_map.is_closed_or_dense_ker

Modified src/topology/algebra/module/finite_dimension.lean

Created src/topology/algebra/module/simple.lean

added theorem linear_map.is_closed_or_dense_ker