Commit 2023-08-18 07:22 96928745

View on Github →

feat(LinearPMap): Closure and inverse commute (#6563)

Estimated changes

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

added theorem LinearPMap.closure_inverse_graph

added theorem LinearPMap.inverse_closure

added theorem LinearPMap.inverse_isClosable_iff