dedekind::linear_algebra::IsOrthogonalMatrixCarrier Concept Reference

Carries the operations under which the orthogonality law Mᵀ · M = I makes sense. More...

Concept definition

template<typename M>
concept dedekind::linear_algebra::IsOrthogonalMatrixCarrier = 
    HasMatrixMultiplication<M> && HasInvolutiveTranspose<M>

Detailed Description

Carries the operations under which the orthogonality law Mᵀ · M = I makes sense.

Orthogonal matrices: the cleanest

group-under-multiplication.

An orthogonal matrix satisfies Mᵀ · M = M · Mᵀ = I, so its inverse is its transpose. Orthogonal matrices are not a ring (not additively closed: I + I = 2I fails orthogonality), so IsDivisionRing does not fire here. They form a multiplicative group O(n, F):

• closed under multiplication: (AB)ᵀ(AB) = BᵀAᵀAB = BᵀIB = I,
• identity I ∈ O(n),
• inverse M⁻¹ = Mᵀ ∈ O(n).

Structurally the concept asks only for matrix multiplication plus an involutive transpose; the orthogonality relation MᵀM = I itself is a value-level law, witnessed per-instance on concrete matrices.

Orthogonality is a per-value predicate (concretely witnessed via static_assert(m.transpose() * m == Identity{})). The concept only pins the structural surface; the law is a theorem about specific carriers and specific values.