Commit 2022-11-12 22:46 f0f3d964

feat(linear_algebra/{basic, affine_space/restrict}): better support for restriction of affine and linear maps (#16397)

• Generalizes linear_map.restrict to allow independent but simultaneous restriction of domain and codomain in a backwards compatible way (except for one type inference failure in algebra.lie.of_associative that had to be fixed manually).
• Adds linear_map.restrict' as an alternative to linear_map.restrict that takes a proof that the image of the new domain must be contained in the new codomain.
• Introduces affine_map.restrict for restriction of affine maps in a new file called linear_algebra/affine_space/restrict.lean and lemmata about injectivity, surjectivity and the coercion of a restricted map. Design choice: A new file restrict.lean was created because affine_subspace.lean is already very long and affine_map.lean does not know about affine maps.