mathlib

580e1d95 - feat(analysis/inner_product_space/pi_L2): `linear_isometry.extend` (#12192)

feat(analysis/inner_product_space/pi_L2): `linear_isometry.extend` (#12192) Let `S` be a subspace of a finite-dimensional inner product space `V`. A linear isometry mapping `S` into `V` can be extended to a full isometry of `V`. Note that this is false if we remove the finite-dimensional hypothesis; consider the shift operator (0, x_2, x_3, ...) to (x_2, x_3, x_4, ...). I hope that the naming choice is consistent. Combining the two `simp only` blocks in `linear_isometry.extend_apply` results in a timeout, but they seem to work okay split up. Co-authored-by: Daniel Packer Co-authored-by: Daniel Packer <62404584+Daniel-Packer@users.noreply.github.com> Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com>