Grace/Cumulus/Rotation/Determinant.g17

Open in Workbench Download source

Imports

Orthogonal · Algebra.Ring.DeterminantThree

Declarations

• realRing.neg_value theorem derivation
• Matrix.ring_matrix theorem derivation
• determinant3.det theorem derivation

Source

1-- The explicit 3 × 3 determinant of the rotation group agrees with the2-- general determinant of the matrix ring over the reals, so the general3-- theory of determinants applies to SO34-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Rotation.Determinant10import Orthogonal11import Algebra.Ring.DeterminantThree1213-- The negation of realRing is the real negation.14theorem realRing.neg_value (x : Set)15  shows Ring.neg(realRing)(x) = -(x:R)16proof17  simp [realRing, Ring.mk.neg]1819-- A 3 × 3 real matrix is a ring matrix over the carrier of realRing.20theorem Matrix.ring_matrix (M : realRing ^ 3 × 3)21  shows RingMatrix(3, Ring.carrier(realRing), M)22proof23  unfold RingMatrix24  exact Matrix.function with *2526-- The explicit determinant is the general one.27theorem determinant3.det (M : realRing ^ 3 × 3)28  shows determinant3(M) = det(M)29proof30  have parts := CommRing.parts with realRing.comm_ring31  have matrix := Matrix.ring_matrix with *32  have expansion := determinant.three at Ring.carrier(realRing), Ring.add(realRing),33    Ring.zero(realRing), Ring.neg(realRing), Ring.mul(realRing), Ring.one(realRing), M34    with parts, matrix35  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ := Matrix.entries_real with *36  rw [determinant3.value, expansion]37  simp [realRing.add_value, realRing.mul_value, realRing.neg_value, realRing.one_value]38  ring39