mathlib

9c8bc915 - feat(linear_algebra/linear_pmap): construct a `linear_pmap` from its graph (#14922)

feat(linear_algebra/linear_pmap): construct a `linear_pmap` from its graph (#14922) Define a partial linear map from its graph. This is a key step in constructing the closure of an linear operator.