mathlib3

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

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.