Documentation

Mathlib.Topology.Algebra.Module.Simple

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.

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.