LinearMap.isClosed_or_dense_ker

theorem LinearMap.isClosed_or_dense_ker : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : TopologicalSpace M] [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : ContinuousSMul R M] [inst_7 : Module R N] [inst_8 : ContinuousAdd M] [inst_9 : IsSimpleModule R N] (l : M →ₗ[R] N), IsClosed ↑(LinearMap.ker l) ∨ Dense ↑(LinearMap.ker l)

The theorem `LinearMap.isClosed_or_dense_ker` states that for any ring `R`, any type `M` with a topological space structure, additive commutative group structure, a module structure over `R`, and continuous scalar multiplication, and any type `N` with an additive commutative group structure, a module structure over `R`, and which is a simple module over `R`, for any linear map `l` from `M` to `N`, the kernel of the linear map `l` (which is a subset of `M`) is either a closed set or a dense set in `M`. This theorem can be applied, for instance, when `R = N` is a division ring.

More concisely: For any continuous linear map between topological vector spaces over a division ring, the kernel is either closed or dense.