mathlib

5de765c5 - feat(linear_algebra/linear_pmap): definition of the graph (#14920)

feat(linear_algebra/linear_pmap): definition of the graph (#14920) Define the graph of a partial linear map as the pushforward of the graph of the underlying linear map and prove some elementary facts. Co-authored-by: Moritz Doll <doll@uni-bremen.de> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>