-- The two generating rotations: rotA about the x-axis and rotB about the
-- z-axis, both by the angle with cosine 3/5 and sine 4/5, their transposes
-- as inverses, and their membership in 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.Generators
import Orthogonal

-- Selecting one of two or three values by an index.
def pick2 (x y : Set, i : Nat) → Set
  | x, y, zero => x
  | x, y, succ(k) => y

def pick3 (x y z : Set, i : Nat) → Set
  | x, y, z, zero => x
  | x, y, z, succ(k) => pick2(y, z, k)

theorem pick3.zero (x y z : Set)
  shows pick3(x, y, z, 0) = x
proof
  simp [pick3]

theorem pick3.one (x y z : Set)
  shows pick3(x, y, z, 1) = y
proof
  simp [pick3, pick2]

theorem pick3.two (x y z : Set)
  shows pick3(x, y, z, 2) = z
proof
  simp [pick3, pick2]

theorem pick3.real (x y z i : Set)
  requires realX : x ∈ ℝ
  requires realY : y ∈ ℝ
  requires realZ : z ∈ ℝ
  requires index : i ∈ 3
  shows pick3(x, y, z, i) ∈ ℝ
proof
  have alternatives := index.cases with index
  rcases alternatives with at0 | at1 | at2
  . rw [at0, pick3.zero]
    exact realX
  . rw [at1, pick3.one]
    exact realY
  . rw [at2, pick3.two]
    exact realZ

-- The entry in row i and column j of the matrix with rows (a, b, c),
-- (d, e, f), (g, h, k), and the matrix itself.
def rowsEntry (a b c d e f g h k i j : Set) : Set :=
  pick3(pick3(a, b, c, j), pick3(d, e, f, j), pick3(g, h, k, j), i)

defgraph mat3 (a b c d e f g h k : Real) (p ∈ 3 × 3) : ℝ :=
  rowsEntry(a, b, c, d, e, f, g, h, k, fst(p), snd(p))
proof
  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with member
  rw [shape, fst.pair, snd.pair]
  have row0 := pick3.real at a, b, c, j with *
  have row1 := pick3.real at d, e, f, j with *
  have row2 := pick3.real at g, h, k, j with *
  unfold rowsEntry
  exact pick3.real with row0, row1, row2, hi

section Entries
variable (a b c d e f g h k : Real)

instance mat3.matrix
  shows mat3(a, b, c, d, e, f, g, h, k) : realRing ^ 3 × 3
proof
  have function := mat3.function at a, b, c, d, e, f, g, h, k with *
  rw ← realRing.carrierOf at function
  exact Matrix.of_function with function

theorem mat3.entry (i j : Set)
  requires row : i ∈ 3
  requires column : j ∈ 3
  shows mat3(a, b, c, d, e, f, g, h, k)[i, j] = rowsEntry(a, b, c, d, e, f, g, h, k, i, j)
proof
  have pair := product.pair at i, j, 3, 3 with *
  have value := mat3.value at a, b, c, d, e, f, g, h, k, (i, j) with *
  rw [value, fst.pair, snd.pair]
  rfl

theorem mat3.e00
  shows mat3(a, b, c, d, e, f, g, h, k)[0, 0] = a
proof
  rw mat3.entry
  simp [rowsEntry, pick3.zero]

theorem mat3.e01
  shows mat3(a, b, c, d, e, f, g, h, k)[0, 1] = b
proof
  rw mat3.entry
  simp [rowsEntry, pick3.zero, pick3.one]

theorem mat3.e02
  shows mat3(a, b, c, d, e, f, g, h, k)[0, 2] = c
proof
  rw mat3.entry
  simp [rowsEntry, pick3.zero, pick3.two]

theorem mat3.e10
  shows mat3(a, b, c, d, e, f, g, h, k)[1, 0] = d
proof
  rw mat3.entry
  simp [rowsEntry, pick3.zero, pick3.one]

theorem mat3.e11
  shows mat3(a, b, c, d, e, f, g, h, k)[1, 1] = e
proof
  rw mat3.entry
  simp [rowsEntry, pick3.one]

theorem mat3.e12
  shows mat3(a, b, c, d, e, f, g, h, k)[1, 2] = f
proof
  rw mat3.entry
  simp [rowsEntry, pick3.one, pick3.two]

theorem mat3.e20
  shows mat3(a, b, c, d, e, f, g, h, k)[2, 0] = g
proof
  rw mat3.entry
  simp [rowsEntry, pick3.zero, pick3.two]

theorem mat3.e21
  shows mat3(a, b, c, d, e, f, g, h, k)[2, 1] = h
proof
  rw mat3.entry
  simp [rowsEntry, pick3.one, pick3.two]

theorem mat3.e22
  shows mat3(a, b, c, d, e, f, g, h, k)[2, 2] = k
proof
  rw mat3.entry
  simp [rowsEntry, pick3.two]

end Entries

-- One fifth, the reciprocal of 5, so that 3/5 = 3 · fifth and 4/5 = 4 · fifth.
def fifth : Set := realInvValue(5)

instance fifth.real
  shows fifth ∈ ℝ
proof
  unfold fifth
  typecheck

theorem fifth.five
  shows fifth * 5 = 1
proof
  have nonzero : (5:R) ≠ 0
    intro equal
    linarith
  have real : (5:R) ∈ ℝ by typecheck
  unfold fifth
  exact realInvValue.mul_left at (5:R) with nonzero

theorem fifth.three
  shows (3:R) / 5 = 3 * fifth
proof
  unfold fifth
  exact realDiv.eq_mul_inv at (3:R), (5:R) with *

theorem fifth.four
  shows (4:R) / 5 = 4 * fifth
proof
  unfold fifth
  exact realDiv.eq_mul_inv at (4:R), (5:R) with *

-- The rotations: rotA about the x-axis, rotB about the z-axis.
def rotA : Set := mat3(1, 0, 0, 0, 3 / 5, -(4 / 5), 0, 4 / 5, 3 / 5)
def rotB : Set := mat3(3 / 5, -(4 / 5), 0, 4 / 5, 3 / 5, 0, 0, 0, 1)

instance rotA.matrix
  shows rotA : realRing ^ 3 × 3
proof
  unfold rotA
  exact mat3.matrix with *

instance rotB.matrix
  shows rotB : realRing ^ 3 × 3
proof
  unfold rotB
  exact mat3.matrix with *

theorem fifth.square
  shows fifth * 5 * (fifth * 5) = 1
proof
  rw fifth.five
  ring

-- Orthogonality from the twelve dot products of columns and of rows.
theorem Orthogonal.of_entries (M : realRing ^ 3 × 3)
  requires c00 : (M[0, 0]:R) * (M[0, 0]:R) + (M[1, 0]:R) * (M[1, 0]:R) + (M[2, 0]:R) * (M[2, 0]:R) = 1
  requires c11 : (M[0, 1]:R) * (M[0, 1]:R) + (M[1, 1]:R) * (M[1, 1]:R) + (M[2, 1]:R) * (M[2, 1]:R) = 1
  requires c22 : (M[0, 2]:R) * (M[0, 2]:R) + (M[1, 2]:R) * (M[1, 2]:R) + (M[2, 2]:R) * (M[2, 2]:R) = 1
  requires c01 : (M[0, 0]:R) * (M[0, 1]:R) + (M[1, 0]:R) * (M[1, 1]:R) + (M[2, 0]:R) * (M[2, 1]:R) = 0
  requires c02 : (M[0, 0]:R) * (M[0, 2]:R) + (M[1, 0]:R) * (M[1, 2]:R) + (M[2, 0]:R) * (M[2, 2]:R) = 0
  requires c12 : (M[0, 1]:R) * (M[0, 2]:R) + (M[1, 1]:R) * (M[1, 2]:R) + (M[2, 1]:R) * (M[2, 2]:R) = 0
  requires r00 : (M[0, 0]:R) * (M[0, 0]:R) + (M[0, 1]:R) * (M[0, 1]:R) + (M[0, 2]:R) * (M[0, 2]:R) = 1
  requires r11 : (M[1, 0]:R) * (M[1, 0]:R) + (M[1, 1]:R) * (M[1, 1]:R) + (M[1, 2]:R) * (M[1, 2]:R) = 1
  requires r22 : (M[2, 0]:R) * (M[2, 0]:R) + (M[2, 1]:R) * (M[2, 1]:R) + (M[2, 2]:R) * (M[2, 2]:R) = 1
  requires r01 : (M[0, 0]:R) * (M[1, 0]:R) + (M[0, 1]:R) * (M[1, 1]:R) + (M[0, 2]:R) * (M[1, 2]:R) = 0
  requires r02 : (M[0, 0]:R) * (M[2, 0]:R) + (M[0, 1]:R) * (M[2, 1]:R) + (M[0, 2]:R) * (M[2, 2]:R) = 0
  requires r12 : (M[1, 0]:R) * (M[2, 0]:R) + (M[1, 1]:R) * (M[2, 1]:R) + (M[1, 2]:R) * (M[2, 2]:R) = 0
  shows Orthogonal(M)
proof
  have comm := realRing.comm_ring
  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ := Matrix.entries_real with *
  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *
  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *
  have same0 : 0 = 0 by rfl
  have same1 : 1 = 1 by rfl
  have same2 : 2 = 2 by rfl
  have s00 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 0, 0 with zeroIn, oneIn, same0
  have s11 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 1, 1 with zeroIn, oneIn, same1
  have s22 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 2, 2 with zeroIn, oneIn, same2
  have s10 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 1, 0 with zeroIn, oneIn, index.zero_ne_one
  have s20 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 2, 0 with zeroIn, oneIn, index.zero_ne_two
  have s01 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 0, 1 with zeroIn, oneIn, index.one_ne_zero
  have s21 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 2, 1 with zeroIn, oneIn, index.one_ne_two
  have s02 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 0, 2 with zeroIn, oneIn, index.two_ne_zero
  have s12 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 1, 2 with zeroIn, oneIn, index.two_ne_one
  have transposed := transpose.matrix at M with *
  have leftProduct := Matrix.mul_matrix at transpose(M), M with *
  have rightProduct := Matrix.mul_matrix at M, transpose(M) with *
  have one := Matrix.one_matrix
  apply Orthogonal.mk
  . apply Matrix.ext with leftProduct, one
    intros j hj k hk
    have entry := matrixRing.mul_entry_three at transpose(M), M, j, k with *
    have unit := matrixRing.one_entry at realRing, 3, j, k with *
    have t0 := transpose.entry at M, j, 0 with *
    have t1 := transpose.entry at M, j, 1 with *
    have t2 := transpose.entry at M, j, 2 with *
    rw [entry, unit, t0, t1, t2]
    have casesJ := index.cases with hj
    have casesK := index.cases with hk
    rcases casesJ with j0 | j1 | j2
    . rcases casesK with k0 | k1 | k2
      . rw [j0, k0, s00, realRing.one_value]
        exact c00
      . rw [j0, k1, s10, realRing.zero_value]
        exact c01
      . rw [j0, k2, s20, realRing.zero_value]
        exact c02
    . rcases casesK with k0 | k1 | k2
      . rw [j1, k0, s01, realRing.zero_value]
        calc
          (M[0, 1]:R) * (M[0, 0]:R) + (M[1, 1]:R) * (M[1, 0]:R) + (M[2, 1]:R) * (M[2, 0]:R) =
            (M[0, 0]:R) * (M[0, 1]:R) + (M[1, 0]:R) * (M[1, 1]:R) + (M[2, 0]:R) * (M[2, 1]:R) := by ring
          _ = 0 := c01
      . rw [j1, k1, s11, realRing.one_value]
        exact c11
      . rw [j1, k2, s21, realRing.zero_value]
        exact c12
    . rcases casesK with k0 | k1 | k2
      . rw [j2, k0, s02, realRing.zero_value]
        calc
          (M[0, 2]:R) * (M[0, 0]:R) + (M[1, 2]:R) * (M[1, 0]:R) + (M[2, 2]:R) * (M[2, 0]:R) =
            (M[0, 0]:R) * (M[0, 2]:R) + (M[1, 0]:R) * (M[1, 2]:R) + (M[2, 0]:R) * (M[2, 2]:R) := by ring
          _ = 0 := c02
      . rw [j2, k1, s12, realRing.zero_value]
        calc
          (M[0, 2]:R) * (M[0, 1]:R) + (M[1, 2]:R) * (M[1, 1]:R) + (M[2, 2]:R) * (M[2, 1]:R) =
            (M[0, 1]:R) * (M[0, 2]:R) + (M[1, 1]:R) * (M[1, 2]:R) + (M[2, 1]:R) * (M[2, 2]:R) := by ring
          _ = 0 := c12
      . rw [j2, k2, s22, realRing.one_value]
        exact c22
  . apply Matrix.ext with rightProduct, one
    intros j hj k hk
    have entry := matrixRing.mul_entry_three at M, transpose(M), j, k with *
    have unit := matrixRing.one_entry at realRing, 3, j, k with *
    have t0 := transpose.entry at M, 0, k with *
    have t1 := transpose.entry at M, 1, k with *
    have t2 := transpose.entry at M, 2, k with *
    rw [entry, unit, t0, t1, t2]
    have casesJ := index.cases with hj
    have casesK := index.cases with hk
    rcases casesJ with j0 | j1 | j2
    . rcases casesK with k0 | k1 | k2
      . rw [j0, k0, s00, realRing.one_value]
        exact r00
      . rw [j0, k1, s10, realRing.zero_value]
        exact r01
      . rw [j0, k2, s20, realRing.zero_value]
        exact r02
    . rcases casesK with k0 | k1 | k2
      . rw [j1, k0, s01, realRing.zero_value]
        calc
          (M[1, 0]:R) * (M[0, 0]:R) + (M[1, 1]:R) * (M[0, 1]:R) + (M[1, 2]:R) * (M[0, 2]:R) =
            (M[0, 0]:R) * (M[1, 0]:R) + (M[0, 1]:R) * (M[1, 1]:R) + (M[0, 2]:R) * (M[1, 2]:R) := by ring
          _ = 0 := r01
      . rw [j1, k1, s11, realRing.one_value]
        exact r11
      . rw [j1, k2, s21, realRing.zero_value]
        exact r12
    . rcases casesK with k0 | k1 | k2
      . rw [j2, k0, s02, realRing.zero_value]
        calc
          (M[2, 0]:R) * (M[0, 0]:R) + (M[2, 1]:R) * (M[0, 1]:R) + (M[2, 2]:R) * (M[0, 2]:R) =
            (M[0, 0]:R) * (M[2, 0]:R) + (M[0, 1]:R) * (M[2, 1]:R) + (M[0, 2]:R) * (M[2, 2]:R) := by ring
          _ = 0 := r02
      . rw [j2, k1, s12, realRing.zero_value]
        calc
          (M[2, 0]:R) * (M[1, 0]:R) + (M[2, 1]:R) * (M[1, 1]:R) + (M[2, 2]:R) * (M[1, 2]:R) =
            (M[1, 0]:R) * (M[2, 0]:R) + (M[1, 1]:R) * (M[2, 1]:R) + (M[1, 2]:R) * (M[2, 2]:R) := by ring
          _ = 0 := r12
      . rw [j2, k2, s22, realRing.one_value]
        exact r22

-- The entries of the two rotations.
theorem rotA.entries
  shows rotA[0, 0] = (1:R) ∧ rotA[0, 1] = (0:R) ∧ rotA[0, 2] = (0:R) ∧
    rotA[1, 0] = (0:R) ∧ rotA[1, 1] = 3 * fifth ∧ rotA[1, 2] = -(4 * fifth) ∧
    rotA[2, 0] = (0:R) ∧ rotA[2, 1] = 4 * fifth ∧ rotA[2, 2] = 3 * fifth
proof
  have e00 := mat3.e00 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),
    (4:R) / 5, (3:R) / 5 with *
  have e01 := mat3.e01 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),
    (4:R) / 5, (3:R) / 5 with *
  have e02 := mat3.e02 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),
    (4:R) / 5, (3:R) / 5 with *
  have e10 := mat3.e10 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),
    (4:R) / 5, (3:R) / 5 with *
  have e11 := mat3.e11 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),
    (4:R) / 5, (3:R) / 5 with *
  have e12 := mat3.e12 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),
    (4:R) / 5, (3:R) / 5 with *
  have e20 := mat3.e20 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),
    (4:R) / 5, (3:R) / 5 with *
  have e21 := mat3.e21 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),
    (4:R) / 5, (3:R) / 5 with *
  have e22 := mat3.e22 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),
    (4:R) / 5, (3:R) / 5 with *
  have unfoldA : rotA = mat3((1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),
      (4:R) / 5, (3:R) / 5)
    simp [rotA]
  rw [unfoldA, e00, e01, e02, e10, e11, e12, e20, e21, e22, fifth.three, fifth.four]
  simp

theorem rotB.entries
  shows rotB[0, 0] = 3 * fifth ∧ rotB[0, 1] = -(4 * fifth) ∧ rotB[0, 2] = (0:R) ∧
    rotB[1, 0] = 4 * fifth ∧ rotB[1, 1] = 3 * fifth ∧ rotB[1, 2] = (0:R) ∧
    rotB[2, 0] = (0:R) ∧ rotB[2, 1] = (0:R) ∧ rotB[2, 2] = (1:R)
proof
  have e00 := mat3.e00 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),
    (0:R), (0:R), (1:R) with *
  have e01 := mat3.e01 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),
    (0:R), (0:R), (1:R) with *
  have e02 := mat3.e02 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),
    (0:R), (0:R), (1:R) with *
  have e10 := mat3.e10 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),
    (0:R), (0:R), (1:R) with *
  have e11 := mat3.e11 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),
    (0:R), (0:R), (1:R) with *
  have e12 := mat3.e12 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),
    (0:R), (0:R), (1:R) with *
  have e20 := mat3.e20 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),
    (0:R), (0:R), (1:R) with *
  have e21 := mat3.e21 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),
    (0:R), (0:R), (1:R) with *
  have e22 := mat3.e22 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),
    (0:R), (0:R), (1:R) with *
  have unfoldB : rotB = mat3((3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),
      (0:R), (0:R), (1:R))
    simp [rotB]
  rw [unfoldB, e00, e01, e02, e10, e11, e12, e20, e21, e22, fifth.three, fifth.four]
  simp

-- rotA and rotB are special orthogonal, with their transposes as inverses;
-- the products with the transpose are written by name, since the closed
-- instances of rotA leave the infix product ambiguous.
theorem rotA.orthogonal
  shows Orthogonal(rotA)
proof
  obtain ⟨a00, a01, a02, a10, a11, a12, a20, a21, a22⟩ := rotA.entries
  have square := fifth.square
  apply Orthogonal.of_entries with rotA.matrix
  . rw [a00, a10, a20]
    ring
  . rw [a01, a11, a21]
    rw ← square
    ring
  . rw [a02, a12, a22]
    rw ← square
    ring
  . rw [a00, a01, a10, a11, a20, a21]
    ring
  . rw [a00, a02, a10, a12, a20, a22]
    ring
  . rw [a01, a02, a11, a12, a21, a22]
    ring
  . rw [a00, a01, a02]
    ring
  . rw [a10, a11, a12]
    rw ← square
    ring
  . rw [a20, a21, a22]
    rw ← square
    ring
  . rw [a00, a01, a02, a10, a11, a12]
    ring
  . rw [a00, a01, a02, a20, a21, a22]
    ring
  . rw [a10, a11, a12, a20, a21, a22]
    ring

theorem rotB.orthogonal
  shows Orthogonal(rotB)
proof
  obtain ⟨b00, b01, b02, b10, b11, b12, b20, b21, b22⟩ := rotB.entries
  have square := fifth.square
  apply Orthogonal.of_entries with rotB.matrix
  . rw [b00, b10, b20]
    rw ← square
    ring
  . rw [b01, b11, b21]
    rw ← square
    ring
  . rw [b02, b12, b22]
    ring
  . rw [b00, b01, b10, b11, b20, b21]
    ring
  . rw [b00, b02, b10, b12, b20, b22]
    ring
  . rw [b01, b02, b11, b12, b21, b22]
    ring
  . rw [b00, b01, b02]
    rw ← square
    ring
  . rw [b10, b11, b12]
    rw ← square
    ring
  . rw [b20, b21, b22]
    ring
  . rw [b00, b01, b02, b10, b11, b12]
    ring
  . rw [b00, b01, b02, b20, b21, b22]
    ring
  . rw [b10, b11, b12, b20, b21, b22]
    ring

theorem rotA.determinant
  shows determinant3(rotA) = (1:R)
proof
  obtain ⟨a00, a01, a02, a10, a11, a12, a20, a21, a22⟩ := rotA.entries
  have square := fifth.square
  rw determinant3.value
  rw ← square
  rw [a00, a01, a02, a10, a11, a12, a20, a21, a22]
  ring

theorem rotB.determinant
  shows determinant3(rotB) = (1:R)
proof
  obtain ⟨b00, b01, b02, b10, b11, b12, b20, b21, b22⟩ := rotB.entries
  have square := fifth.square
  rw determinant3.value
  rw ← square
  rw [b00, b01, b02, b10, b11, b12, b20, b21, b22]
  ring

theorem rotA.so3
  shows rotA ∈ so3Matrices
proof
  exact so3Matrices.mk with rotA.orthogonal, rotA.determinant

theorem rotB.so3
  shows rotB ∈ so3Matrices
proof
  exact so3Matrices.mk with rotB.orthogonal, rotB.determinant

theorem rotA.transpose_so3
  shows transpose(rotA) ∈ so3Matrices
proof
  exact so3Matrices.transpose_mem with rotA.so3

theorem rotB.transpose_so3
  shows transpose(rotB) ∈ so3Matrices
proof
  exact so3Matrices.transpose_mem with rotB.so3

theorem rotA.inverse
  shows so3Inverse(rotA) = transpose(rotA)
proof
  exact so3Inverse.value with rotA.so3

theorem rotB.inverse
  shows so3Inverse(rotB) = transpose(rotB)
proof
  exact so3Inverse.value with rotB.so3

theorem rotA.transpose_mul
  shows Ring.mul(matrixRing(realRing, 3))(transpose(rotA), rotA) =
    Ring.one(matrixRing(realRing, 3))
proof
  exact Orthogonal.left with rotA.orthogonal

theorem rotA.mul_transpose
  shows Ring.mul(matrixRing(realRing, 3))(rotA, transpose(rotA)) =
    Ring.one(matrixRing(realRing, 3))
proof
  exact Orthogonal.right with rotA.orthogonal

theorem rotB.transpose_mul
  shows Ring.mul(matrixRing(realRing, 3))(transpose(rotB), rotB) =
    Ring.one(matrixRing(realRing, 3))
proof
  exact Orthogonal.left with rotB.orthogonal

theorem rotB.mul_transpose
  shows Ring.mul(matrixRing(realRing, 3))(rotB, transpose(rotB)) =
    Ring.one(matrixRing(realRing, 3))
proof
  exact Orthogonal.right with rotB.orthogonal