mathlib

b4a51d92 - feat(topology/algebra/module): add basic definitions for `linear_pmap` in topological vector spaces (#15479)

feat(topology/algebra/module): add basic definitions for `linear_pmap` in topological vector spaces (#15479) We define closed, closable operators, the closure, and cores. All these definitions are valid on topological vector spaces. Co-authored-by: Moritz Doll <doll@uni-bremen.de>