Theorem LinearPMap.inverse_closed_iff

Modification history

2026-08-16 23:56
Mathlib/Topology/Algebra/Module/LinearPMap.lean
feat(LinearAlgebra): kernel of a `LinearPMap` (#42423) …
Modified LinearPMap.inverse_closed_iffView on Github →
2025-09-16 11:11
Mathlib/Topology/Algebra/Module/LinearPMap.lean
feat(Topology/LinearPMap): the inverse is closed iff f is closed (#29631) …
Added LinearPMap.inverse_closed_iffView on Github →