# 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.