linearEquiv_det_rotation
theorem linearEquiv_det_rotation : ∀ (a : ↥circle), LinearEquiv.det (rotation a).toLinearEquiv = 1
The theorem `linearEquiv_det_rotation` states that for every element `a` in the unit circle, the determinant of the linear equivalence transformation associated with the rotation by `a` is equal to `1`. This essentially means that the rotation operation, defined by any point on the unit circle in the complex plane, preserves volume (reflected by the determinant being `1`), thus making it an isometry.
More concisely: The determinant of the linear transformation representing rotation by an angle in the complex plane is equal to 1.
|
det_rotation
theorem det_rotation : ∀ (a : ↥circle), LinearMap.det ↑(rotation a).toLinearEquiv = 1
This theorem states that the determinant of the rotation operation, when considered as a linear map, is always equal to 1 for any element in the unit circle. The rotation operation is defined by mapping an element of the unit circle to a linear isometry equivalence (which effectively preserves lengths and angles) from the complex numbers to themselves. Thus, this theorem asserts the invariance of the determinant under such a rotation operation.
More concisely: The determinant of a linear isometry (rotation) mapping complex numbers on the unit circle to themselves is equal to 1.
|
toMatrix_rotation
theorem toMatrix_rotation :
∀ (a : ↥circle),
(LinearMap.toMatrix Complex.basisOneI Complex.basisOneI) ↑(rotation a).toLinearEquiv =
↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯)
This theorem states that for any element 'a' of the unit circle, the matrix representation of the rotation corresponding to 'a' is equal to the conformal matrix with entries corresponding to the real and imaginary parts of 'a'. In more mathematical terms, if we consider the unit circle in the complex plane, each point 'a' on it defines a rotation of the plane. This rotation can be represented as a matrix with respect to the basis `1` and `I` of the complex numbers over the real numbers. The theorem claims that this matrix is the same as the one defined by `[Re(a), -Im(a); Im(a), Re(a)]`, provided the sum of the squares of the real part and the imaginary part of 'a' is non-zero.
More concisely: For any complex number 'a' on the unit circle, the matrix representation of the corresponding rotation is equal to `[Re(a), -Im(a); Im(a), Re(a)]`.
|