mathlib3

c0c910de - feat(linear_algebra/linear_pmap): more lemmas about the graph (#15531)

feat(linear_algebra/linear_pmap): more lemmas about the graph (#15531) This PR adds more lemmas about the graph of a partially defined linear map, in particular about scalar multiplication and negation of `linear_pmap`s as well as relating inequalities and equalities between the graph and the `linear_pmap`.