Real coordinates of the complex plane

The real linear coordinate interchange is an involution with determinant -1, recording the reversal of orientation.

noncomputable def Complex.coordinateSwapCLE : ℂ ≃L[ℝ] ℂ

The real continuous linear equivalence interchanging real and imaginary coordinates.

Equations

• Complex.coordinateSwapCLE = (Complex.equivRealProdCLM.trans (ContinuousLinearEquiv.prodComm ℝ ℝ ℝ)).trans Complex.equivRealProdCLM.symm

@[simp]

theorem Complex.coordinateSwapCLE_apply (z : ℂ) : coordinateSwapCLE z = { re := z.im, im := z.re }

Coordinate swap sends (x,y) to (y,x).

@[simp]

theorem Complex.coordinateSwapCLE_symm : coordinateSwapCLE.symm = coordinateSwapCLE

Coordinate interchange is its own inverse.

theorem Complex.coordinateSwapCLE_coordinateSwapCLE (z : ℂ) : coordinateSwapCLE (coordinateSwapCLE z) = z

Interchanging the coordinates twice returns the original point.

@[simp]

theorem Complex.det_coordinateSwapCLE : LinearMap.det ↑↑coordinateSwapCLE = -1

Interchanging the coordinates has real determinant -1.

@[simp]

theorem Complex.linearEquiv_det_coordinateSwapCLE : LinearEquiv.det ↑coordinateSwapCLE = -1

The determinant unit of coordinate interchange is -1.