Commit 2023-08-03 09:17 daafa2f6

View on Github →

refactor: use junk values in Submodule.toLinearPMap (#5529) Change the definition of Submodule.toLinearPMap to use a junk value in the case that the condition that the subspace defines the graph of a function is not satisfied. In this case we define Submodule.toLinearPMap as the zero map. The domain is the same so that the domain does not depend on the graph-condition.

Estimated changes

Modified Mathlib/LinearAlgebra/LinearPMap.lean

modified theorem LinearPMap.inverse_apply_eq

modified theorem LinearPMap.inverse_domain

modified theorem LinearPMap.inverse_graph

modified theorem LinearPMap.inverse_range

modified theorem LinearPMap.mem_inverse_graph

added theorem LinearPMap.mem_inverse_graph_snd_eq_zero

modified theorem Submodule.mem_graph_toLinearPMap

added theorem Submodule.toLinearPMap_apply_aux

modified theorem Submodule.toLinearPMap_domain

Modified Mathlib/Topology/Algebra/Module/LinearPMap.lean