Physlib.Mathematics.OrthogonalMatrix

Orthogonal matrices and the dot product

An orthogonal matrix — a square matrix `A` with `Aᵀ A = 1` — preserves the dot product of vectors, and in particular their squared lengths. This is the algebraic content behind the frame-independence of the *rotational* kinetic energy in rigid-body dynamics: rotating a velocity does not change its speed.

1 declaration

theorem

Orthogonal Matrices Preserve the Dot Product: $(A v) \cdot (A w) = v \cdot w$

#dotProduct_mulVec_orthogonal

Let $R$ be a commutative ring and $n$ be a finite index set. For any $n \times n$ matrix $A$ over $R$ that is orthogonal, meaning $A^\top A = I$ (where $I$ is the identity matrix), and for any vectors $v, w \in R^n$ , the dot product of the transformed vectors is equal to the dot product of the original vectors: $(A v) \cdot (A w) = v \cdot w$

Physlib.Mathematics.OrthogonalMatrix

Orthogonal matrices and the dot product

Orthogonal Matrices Preserve the Dot Product: (Av)⋅(Aw)=v⋅w(A v) \cdot (A w) = v \cdot w(Av)⋅(Aw)=v⋅w

Orthogonal Matrices Preserve the Dot Product: $(A v) \cdot (A w) = v \cdot w$