Commit 2022-07-21 18:20 c0c910de

View on Github →

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_pmaps as well as relating inequalities and equalities between the graph and the linear_pmap.

Estimated changes

Modified src/linear_algebra/linear_pmap.lean

added theorem linear_pmap.eq_of_eq_graph

added theorem linear_pmap.image_iff

added theorem linear_pmap.le_of_le_graph

added theorem linear_pmap.mem_domain_iff

added theorem linear_pmap.mem_domain_iff_of_eq_graph

added theorem linear_pmap.mem_range_iff

added theorem linear_pmap.neg_graph

added theorem linear_pmap.smul_graph