mathlib3

09258fb7 - feat(analysis/normed_space/affine_isometry, linear_algebra/affine_space/affine_equiv): restrict affine isometry to isometry equivalence (#17522)

feat(analysis/normed_space/affine_isometry, linear_algebra/affine_space/affine_equiv): restrict affine isometry to isometry equivalence (#17522) The main result in this commit is `affine_subspace.isometry_equiv_map`: Given an affine isometry, each of its affine subspaces is affine isometry equivalent to its image. `isometry_equiv_map` returns this isometry equivalence. The two other most significant results that are proved on the way are: - `affine_subspace.equiv_map_of_injective`: Restricts an injective affine map to an affine equivalence of a subspace to its image (used by `isometry_equiv_map`) - `affine_equiv.of_bijective`: obtain an affine equivalence from a bijective affine map The construction uses the new definition `affine_equiv.of_bijective` that makes an affine equivalence of a bijective affine map. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>