Commit 2023-04-20 11:28 e0fa506a

View on Github →

feat: inverse of LinearPMap (#3527)

Estimated changes

Modified Mathlib/LinearAlgebra/LinearPMap.lean

added theorem LinearPMap.graph_map_fst_eq_domain

added theorem LinearPMap.graph_map_snd_eq_range

added theorem LinearPMap.inverse_apply_eq

added theorem LinearPMap.inverse_domain

added theorem LinearPMap.inverse_graph

added theorem LinearPMap.inverse_range

added theorem LinearPMap.mem_inverse_graph

added theorem Submodule.toLinearPMap_domain

added theorem Submodule.toLinearPMap_range

Modified Mathlib/LinearAlgebra/Prod.lean

added theorem LinearEquiv.fst_comp_prodComm

added theorem LinearEquiv.snd_comp_prodComm