The kernel of a linear function is closed or dense

In this file we prove (LinearMap.isClosed_or_dense_ker) that the kernel of a linear function f : M →ₗ[R] N is either closed or dense in M provided that N is a simple module over R. This applies, e.g., to the case when R = N is a division ring.

theorem LinearMap.isClosed_or_dense_ker {R : Type u} {M : Type v} {N : Type w} [Ring R] [TopologicalSpace R] [TopologicalSpace M] [AddCommGroup M] [AddCommGroup N] [Module R M] [ContinuousSMul R M] [Module R N] [ContinuousAdd M] [IsSimpleModule R N] (l : M →ₗ[R] N) : IsClosed ↑(LinearMap.ker l) ∨ Dense ↑(LinearMap.ker l)

The kernel of a linear map taking values in a simple module over the base ring is closed or dense. Applies, e.g., to the case when R = N is a division ring.