mathlib3

58a37203 - feat(analysis/inner_product_space/pi_L2): `complex.isometry_of_orthonormal` (#11970)

feat(analysis/inner_product_space/pi_L2): `complex.isometry_of_orthonormal` (#11970) Add a definition for the isometry between `ℂ` and a two-dimensional real inner product space given by a basis, and an associated `simp` lemma for how this relates to `basis.map`. This definition is just the composition of two existing definitions, `complex.isometry_euclidean` and (the inverse of) `basis.isometry_euclidean_of_orthonormal`. However, it's still useful to have it as a single definition when using it to define and prove basic properties of oriented angles (in an oriented two-dimensional real inner product space), to keep definitions and terms in proofs simpler and to avoid tactics such as `simp` or `rw` rearranging things inside this definition when not wanted (almost everything just needs to use some isometry between these two spaces without caring about the details of how it's defined, so it seems best to use a single `def` for this isometry, and on the rare occasions where the details of how it's defined matter, prove specific lemmas about the required properties).