Complex.det_conjAe
theorem Complex.det_conjAe : LinearMap.det Complex.conjAe.toLinearMap = -1
This theorem states that the determinant of the complex conjugation function, when viewed as a linear map via algebra isomorphism from the set of complex numbers to itself, is equal to -1. The function `Complex.conjAe` is an isomorphism of real-algebra, and its determinant respects the linear map structure. The complex conjugation function flips the sign of the imaginary part of a complex number, which can be interpreted as a reflection (a linear transformation) in the complex plane, and such reflections have determinant -1.
More concisely: The determinant of the complex conjugation function as a linear map, viewed as an isomorphism from the set of complex numbers to itself, equals -1.
|
Complex.linearEquiv_det_conjAe
theorem Complex.linearEquiv_det_conjAe : LinearEquiv.det Complex.conjAe.toLinearEquiv = -1
The theorem `Complex.linearEquiv_det_conjAe` states that the determinant of the complex conjugation function `conjAe` (when viewed as a linear equivalence) is equal to -1. In other words, the linear transformation that corresponds to the complex conjugation operation has a determinant of -1. This means that the transformation flips the orientation of the complex plane.
More concisely: The determinant of the linear equivalence represented by the complex conjugation function is equal to -1.
|