Research proof index

Under the standard chart, the Euclidean action on Space d is the transport of toAffineIsometryMulEquiv acting on EuclideanSpace: chart (g • p) = (toAffineIsometryMulEquiv g) (chart p).

linearIsometryEquivToOrthogonal is a left inverse of orthogonalToLinearIsometryEquiv. Together with linearIsometryEquiv_constVAdd_mul, this proves left_inv of toAffineIsometryMulEquiv.

linearIsometryEquivToOrthogonal is a right inverse of orthogonalToLinearIsometryEquiv; this proves right_inv of toAffineIsometryMulEquiv.

A rotation fixes the origin: its translation part vanishes (RotationGroup ≤ OriginStabilizer), so ↑r • 0 = 0. Stated in the ↑r form (the simp normal form of r • _, via rotation_smul_eq) so it is a well-formed simp lemma.

Triple Euclidean Levi-Civita contraction ∑_h (ε4)_{a,h} · (ε4)_{b,h} = 6 · δ[a,b] at the symbol level: contracting three of the four Fin 4 component slots of ε4 with the naive Kronecker pairing leaves one free pair a, b and the factor 3! = 6. The Lorentz form carries an extra det η = -1.

Double Euclidean Levi-Civita contraction ∑_h (ε4)_{r,s,h} · (ε4)_{t,w,h} = 2 · (δ[r,t]·δ[s,w] - δ[r,w]·δ[s,t]) at the symbol level: contracting two of the four Fin 4 component slots of ε4 with the naive Kronecker pairing leaves two free pairs and the factor 2! = 2. The Lorentz form carries an extra det η = -1.