Commit 2026-08-16 23:56 f5dc2eb2

View on Github →

feat(LinearAlgebra): kernel of a LinearPMap (#42423) We define the kernel of a LinearPMap as a submodule of E and prove basic properties of it. If one takes f.toFun.ker then it is a submodule of f.domain, which leads to many problems. Secondly, the code around LinearPMap.inverse gets cleaned up: use LinearPMap.ker, use dot-notation consistently, and some golfs.

Estimated changes

Modified Mathlib/LinearAlgebra/LinearPMap.lean

added theorem LinearMap.toPMap_ker

added theorem LinearPMap.coe_mem_ker_iff

added theorem LinearPMap.coe_toFun_eq_coe

added theorem LinearPMap.eqLocus_zero

modified theorem LinearPMap.inverse_apply_eq

modified theorem LinearPMap.inverse_domain

modified theorem LinearPMap.inverse_graph

modified theorem LinearPMap.inverse_range

added def LinearPMap.ker

added theorem LinearPMap.ker_eq_bot'

added theorem LinearPMap.ker_eq_bot

added theorem LinearPMap.ker_eq_top

added theorem LinearPMap.ker_le_domain

added theorem LinearPMap.ker_neg

added theorem LinearPMap.ker_zero

modified theorem LinearPMap.mem_inverse_graph

deleted theorem LinearPMap.mem_inverse_graph_snd_eq_zero

added theorem LinearPMap.mem_ker_iff

added theorem LinearPMap.sub_mem_ker_iff

Modified Mathlib/Topology/Algebra/Module/LinearPMap.lean

modified theorem LinearPMap.closure_inverse_graph

modified theorem LinearPMap.inverse_closed_iff

modified theorem LinearPMap.inverse_closure

modified theorem LinearPMap.inverse_isClosable_iff