-- The explicit 3 × 3 determinant of the rotation group agrees with the
-- general determinant of the matrix ring over the reals, so the general
-- theory of determinants applies to SO3
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Rotation.Determinant
import Orthogonal
import Algebra.Ring.DeterminantThree

-- The negation of realRing is the real negation.
theorem realRing.neg_value (x : Set)
  shows Ring.neg(realRing)(x) = -(x:R)
proof
  simp [realRing, Ring.mk.neg]

-- A 3 × 3 real matrix is a ring matrix over the carrier of realRing.
theorem Matrix.ring_matrix (M : realRing ^ 3 × 3)
  shows RingMatrix(3, Ring.carrier(realRing), M)
proof
  unfold RingMatrix
  exact Matrix.function with *

-- The explicit determinant is the general one.
theorem determinant3.det (M : realRing ^ 3 × 3)
  shows determinant3(M) = det(M)
proof
  have parts := CommRing.parts with realRing.comm_ring
  have matrix := Matrix.ring_matrix with *
  have expansion := determinant.three at Ring.carrier(realRing), Ring.add(realRing),
    Ring.zero(realRing), Ring.neg(realRing), Ring.mul(realRing), Ring.one(realRing), M
    with parts, matrix
  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ := Matrix.entries_real with *
  rw [determinant3.value, expansion]
  simp [realRing.add_value, realRing.mul_value, realRing.neg_value, realRing.one_value]
  ring