# Commit 2022-11-12 22:46 f0f3d964

View on Github →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.