Commit 2022-02-17 10:00 58a37203

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