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).







leanprover-community/mathlib,leanprover-community/mathlib