Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-29 14:27 5de765c5

View on Github →

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.

Estimated changes