Grace/Cumulus/Rotation/Generators.g17

Open in Workbench Download source

Imports

Orthogonal

Declarations

Source

1-- The two generating rotations: rotA about the x-axis and rotB about the2-- z-axis, both by the angle with cosine 3/5 and sine 4/5, their transposes3-- as inverses, and their membership in 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.Generators10import Orthogonal1112-- Selecting one of two or three values by an index.13def pick2 (x y : Set, i : Nat) → Set14  | x, y, zero => x15  | x, y, succ(k) => y1617def pick3 (x y z : Set, i : Nat) → Set18  | x, y, z, zero => x19  | x, y, z, succ(k) => pick2(y, z, k)2021theorem pick3.zero (x y z : Set)22  shows pick3(x, y, z, 0) = x23proof24  simp [pick3]2526theorem pick3.one (x y z : Set)27  shows pick3(x, y, z, 1) = y28proof29  simp [pick3, pick2]3031theorem pick3.two (x y z : Set)32  shows pick3(x, y, z, 2) = z33proof34  simp [pick3, pick2]3536theorem pick3.real (x y z i : Set)37  requires realX : x ∈ ℝ38  requires realY : y ∈ ℝ39  requires realZ : z ∈ ℝ40  requires index : i ∈ 341  shows pick3(x, y, z, i) ∈ ℝ42proof43  have alternatives := index.cases with index44  rcases alternatives with at0 | at1 | at245  . rw [at0, pick3.zero]46    exact realX47  . rw [at1, pick3.one]48    exact realY49  . rw [at2, pick3.two]50    exact realZ5152-- The entry in row i and column j of the matrix with rows (a, b, c),53-- (d, e, f), (g, h, k), and the matrix itself.54def rowsEntry (a b c d e f g h k i j : Set) : Set :=55  pick3(pick3(a, b, c, j), pick3(d, e, f, j), pick3(g, h, k, j), i)5657defgraph mat3 (a b c d e f g h k : Real) (p ∈ 3 × 3) : ℝ :=58  rowsEntry(a, b, c, d, e, f, g, h, k, fst(p), snd(p))59proof60  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with member61  rw [shape, fst.pair, snd.pair]62  have row0 := pick3.real at a, b, c, j with *63  have row1 := pick3.real at d, e, f, j with *64  have row2 := pick3.real at g, h, k, j with *65  unfold rowsEntry66  exact pick3.real with row0, row1, row2, hi6768section Entries69variable (a b c d e f g h k : Real)7071instance mat3.matrix72  shows mat3(a, b, c, d, e, f, g, h, k) : realRing ^ 3 × 373proof74  have function := mat3.function at a, b, c, d, e, f, g, h, k with *75  rw ← realRing.carrierOf at function76  exact Matrix.of_function with function7778theorem mat3.entry (i j : Set)79  requires row : i ∈ 380  requires column : j ∈ 381  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)82proof83  have pair := product.pair at i, j, 3, 3 with *84  have value := mat3.value at a, b, c, d, e, f, g, h, k, (i, j) with *85  rw [value, fst.pair, snd.pair]86  rfl8788theorem mat3.e0089  shows mat3(a, b, c, d, e, f, g, h, k)[0, 0] = a90proof91  rw mat3.entry92  simp [rowsEntry, pick3.zero]9394theorem mat3.e0195  shows mat3(a, b, c, d, e, f, g, h, k)[0, 1] = b96proof97  rw mat3.entry98  simp [rowsEntry, pick3.zero, pick3.one]99100theorem mat3.e02101  shows mat3(a, b, c, d, e, f, g, h, k)[0, 2] = c102proof103  rw mat3.entry104  simp [rowsEntry, pick3.zero, pick3.two]105106theorem mat3.e10107  shows mat3(a, b, c, d, e, f, g, h, k)[1, 0] = d108proof109  rw mat3.entry110  simp [rowsEntry, pick3.zero, pick3.one]111112theorem mat3.e11113  shows mat3(a, b, c, d, e, f, g, h, k)[1, 1] = e114proof115  rw mat3.entry116  simp [rowsEntry, pick3.one]117118theorem mat3.e12119  shows mat3(a, b, c, d, e, f, g, h, k)[1, 2] = f120proof121  rw mat3.entry122  simp [rowsEntry, pick3.one, pick3.two]123124theorem mat3.e20125  shows mat3(a, b, c, d, e, f, g, h, k)[2, 0] = g126proof127  rw mat3.entry128  simp [rowsEntry, pick3.zero, pick3.two]129130theorem mat3.e21131  shows mat3(a, b, c, d, e, f, g, h, k)[2, 1] = h132proof133  rw mat3.entry134  simp [rowsEntry, pick3.one, pick3.two]135136theorem mat3.e22137  shows mat3(a, b, c, d, e, f, g, h, k)[2, 2] = k138proof139  rw mat3.entry140  simp [rowsEntry, pick3.two]141142end Entries143144-- One fifth, the reciprocal of 5, so that 3/5 = 3 · fifth and 4/5 = 4 · fifth.145def fifth : Set := realInvValue(5)146147instance fifth.real148  shows fifth ∈ ℝ149proof150  unfold fifth151  typecheck152153theorem fifth.five154  shows fifth * 5 = 1155proof156  have nonzero : (5:R) ≠ 0157    intro equal158    linarith159  have real : (5:R) ∈ ℝ by typecheck160  unfold fifth161  exact realInvValue.mul_left at (5:R) with nonzero162163theorem fifth.three164  shows (3:R) / 5 = 3 * fifth165proof166  unfold fifth167  exact realDiv.eq_mul_inv at (3:R), (5:R) with *168169theorem fifth.four170  shows (4:R) / 5 = 4 * fifth171proof172  unfold fifth173  exact realDiv.eq_mul_inv at (4:R), (5:R) with *174175-- The rotations: rotA about the x-axis, rotB about the z-axis.176def rotA : Set := mat3(1, 0, 0, 0, 3 / 5, -(4 / 5), 0, 4 / 5, 3 / 5)177def rotB : Set := mat3(3 / 5, -(4 / 5), 0, 4 / 5, 3 / 5, 0, 0, 0, 1)178179instance rotA.matrix180  shows rotA : realRing ^ 3 × 3181proof182  unfold rotA183  exact mat3.matrix with *184185instance rotB.matrix186  shows rotB : realRing ^ 3 × 3187proof188  unfold rotB189  exact mat3.matrix with *190191theorem fifth.square192  shows fifth * 5 * (fifth * 5) = 1193proof194  rw fifth.five195  ring196197-- Orthogonality from the twelve dot products of columns and of rows.198theorem Orthogonal.of_entries (M : realRing ^ 3 × 3)199  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) = 1200  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) = 1201  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) = 1202  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) = 0203  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) = 0204  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) = 0205  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) = 1206  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) = 1207  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) = 1208  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) = 0209  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) = 0210  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) = 0211  shows Orthogonal(M)212proof213  have comm := realRing.comm_ring214  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ := Matrix.entries_real with *215  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *216  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *217  have same0 : 0 = 0 by rfl218  have same1 : 1 = 1 by rfl219  have same2 : 2 = 2 by rfl220  have s00 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),221    Ring.one(realRing), 0, 0 with zeroIn, oneIn, same0222  have s11 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),223    Ring.one(realRing), 1, 1 with zeroIn, oneIn, same1224  have s22 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),225    Ring.one(realRing), 2, 2 with zeroIn, oneIn, same2226  have s10 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),227    Ring.one(realRing), 1, 0 with zeroIn, oneIn, index.zero_ne_one228  have s20 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),229    Ring.one(realRing), 2, 0 with zeroIn, oneIn, index.zero_ne_two230  have s01 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),231    Ring.one(realRing), 0, 1 with zeroIn, oneIn, index.one_ne_zero232  have s21 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),233    Ring.one(realRing), 2, 1 with zeroIn, oneIn, index.one_ne_two234  have s02 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),235    Ring.one(realRing), 0, 2 with zeroIn, oneIn, index.two_ne_zero236  have s12 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),237    Ring.one(realRing), 1, 2 with zeroIn, oneIn, index.two_ne_one238  have transposed := transpose.matrix at M with *239  have leftProduct := Matrix.mul_matrix at transpose(M), M with *240  have rightProduct := Matrix.mul_matrix at M, transpose(M) with *241  have one := Matrix.one_matrix242  apply Orthogonal.mk243  . apply Matrix.ext with leftProduct, one244    intros j hj k hk245    have entry := matrixRing.mul_entry_three at transpose(M), M, j, k with *246    have unit := matrixRing.one_entry at realRing, 3, j, k with *247    have t0 := transpose.entry at M, j, 0 with *248    have t1 := transpose.entry at M, j, 1 with *249    have t2 := transpose.entry at M, j, 2 with *250    rw [entry, unit, t0, t1, t2]251    have casesJ := index.cases with hj252    have casesK := index.cases with hk253    rcases casesJ with j0 | j1 | j2254    . rcases casesK with k0 | k1 | k2255      . rw [j0, k0, s00, realRing.one_value]256        exact c00257      . rw [j0, k1, s10, realRing.zero_value]258        exact c01259      . rw [j0, k2, s20, realRing.zero_value]260        exact c02261    . rcases casesK with k0 | k1 | k2262      . rw [j1, k0, s01, realRing.zero_value]263        calc264          (M[0, 1]:R) * (M[0, 0]:R) + (M[1, 1]:R) * (M[1, 0]:R) + (M[2, 1]:R) * (M[2, 0]:R) =265            (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 ring266          _ = 0 := c01267      . rw [j1, k1, s11, realRing.one_value]268        exact c11269      . rw [j1, k2, s21, realRing.zero_value]270        exact c12271    . rcases casesK with k0 | k1 | k2272      . rw [j2, k0, s02, realRing.zero_value]273        calc274          (M[0, 2]:R) * (M[0, 0]:R) + (M[1, 2]:R) * (M[1, 0]:R) + (M[2, 2]:R) * (M[2, 0]:R) =275            (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 ring276          _ = 0 := c02277      . rw [j2, k1, s12, realRing.zero_value]278        calc279          (M[0, 2]:R) * (M[0, 1]:R) + (M[1, 2]:R) * (M[1, 1]:R) + (M[2, 2]:R) * (M[2, 1]:R) =280            (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 ring281          _ = 0 := c12282      . rw [j2, k2, s22, realRing.one_value]283        exact c22284  . apply Matrix.ext with rightProduct, one285    intros j hj k hk286    have entry := matrixRing.mul_entry_three at M, transpose(M), j, k with *287    have unit := matrixRing.one_entry at realRing, 3, j, k with *288    have t0 := transpose.entry at M, 0, k with *289    have t1 := transpose.entry at M, 1, k with *290    have t2 := transpose.entry at M, 2, k with *291    rw [entry, unit, t0, t1, t2]292    have casesJ := index.cases with hj293    have casesK := index.cases with hk294    rcases casesJ with j0 | j1 | j2295    . rcases casesK with k0 | k1 | k2296      . rw [j0, k0, s00, realRing.one_value]297        exact r00298      . rw [j0, k1, s10, realRing.zero_value]299        exact r01300      . rw [j0, k2, s20, realRing.zero_value]301        exact r02302    . rcases casesK with k0 | k1 | k2303      . rw [j1, k0, s01, realRing.zero_value]304        calc305          (M[1, 0]:R) * (M[0, 0]:R) + (M[1, 1]:R) * (M[0, 1]:R) + (M[1, 2]:R) * (M[0, 2]:R) =306            (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 ring307          _ = 0 := r01308      . rw [j1, k1, s11, realRing.one_value]309        exact r11310      . rw [j1, k2, s21, realRing.zero_value]311        exact r12312    . rcases casesK with k0 | k1 | k2313      . rw [j2, k0, s02, realRing.zero_value]314        calc315          (M[2, 0]:R) * (M[0, 0]:R) + (M[2, 1]:R) * (M[0, 1]:R) + (M[2, 2]:R) * (M[0, 2]:R) =316            (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 ring317          _ = 0 := r02318      . rw [j2, k1, s12, realRing.zero_value]319        calc320          (M[2, 0]:R) * (M[1, 0]:R) + (M[2, 1]:R) * (M[1, 1]:R) + (M[2, 2]:R) * (M[1, 2]:R) =321            (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 ring322          _ = 0 := r12323      . rw [j2, k2, s22, realRing.one_value]324        exact r22325326-- The entries of the two rotations.327theorem rotA.entries328  shows rotA[0, 0] = (1:R) ∧ rotA[0, 1] = (0:R) ∧ rotA[0, 2] = (0:R) ∧329    rotA[1, 0] = (0:R) ∧ rotA[1, 1] = 3 * fifth ∧ rotA[1, 2] = -(4 * fifth) ∧330    rotA[2, 0] = (0:R) ∧ rotA[2, 1] = 4 * fifth ∧ rotA[2, 2] = 3 * fifth331proof332  have e00 := mat3.e00 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),333    (4:R) / 5, (3:R) / 5 with *334  have e01 := mat3.e01 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),335    (4:R) / 5, (3:R) / 5 with *336  have e02 := mat3.e02 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),337    (4:R) / 5, (3:R) / 5 with *338  have e10 := mat3.e10 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),339    (4:R) / 5, (3:R) / 5 with *340  have e11 := mat3.e11 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),341    (4:R) / 5, (3:R) / 5 with *342  have e12 := mat3.e12 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),343    (4:R) / 5, (3:R) / 5 with *344  have e20 := mat3.e20 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),345    (4:R) / 5, (3:R) / 5 with *346  have e21 := mat3.e21 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),347    (4:R) / 5, (3:R) / 5 with *348  have e22 := mat3.e22 at (1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),349    (4:R) / 5, (3:R) / 5 with *350  have unfoldA : rotA = mat3((1:R), (0:R), (0:R), (0:R), (3:R) / 5, -((4:R) / 5), (0:R),351      (4:R) / 5, (3:R) / 5)352    simp [rotA]353  rw [unfoldA, e00, e01, e02, e10, e11, e12, e20, e21, e22, fifth.three, fifth.four]354  simp355356theorem rotB.entries357  shows rotB[0, 0] = 3 * fifth ∧ rotB[0, 1] = -(4 * fifth) ∧ rotB[0, 2] = (0:R) ∧358    rotB[1, 0] = 4 * fifth ∧ rotB[1, 1] = 3 * fifth ∧ rotB[1, 2] = (0:R) ∧359    rotB[2, 0] = (0:R) ∧ rotB[2, 1] = (0:R) ∧ rotB[2, 2] = (1:R)360proof361  have e00 := mat3.e00 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),362    (0:R), (0:R), (1:R) with *363  have e01 := mat3.e01 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),364    (0:R), (0:R), (1:R) with *365  have e02 := mat3.e02 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),366    (0:R), (0:R), (1:R) with *367  have e10 := mat3.e10 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),368    (0:R), (0:R), (1:R) with *369  have e11 := mat3.e11 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),370    (0:R), (0:R), (1:R) with *371  have e12 := mat3.e12 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),372    (0:R), (0:R), (1:R) with *373  have e20 := mat3.e20 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),374    (0:R), (0:R), (1:R) with *375  have e21 := mat3.e21 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),376    (0:R), (0:R), (1:R) with *377  have e22 := mat3.e22 at (3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),378    (0:R), (0:R), (1:R) with *379  have unfoldB : rotB = mat3((3:R) / 5, -((4:R) / 5), (0:R), (4:R) / 5, (3:R) / 5, (0:R),380      (0:R), (0:R), (1:R))381    simp [rotB]382  rw [unfoldB, e00, e01, e02, e10, e11, e12, e20, e21, e22, fifth.three, fifth.four]383  simp384385-- rotA and rotB are special orthogonal, with their transposes as inverses;386-- the products with the transpose are written by name, since the closed387-- instances of rotA leave the infix product ambiguous.388theorem rotA.orthogonal389  shows Orthogonal(rotA)390proof391  obtain ⟨a00, a01, a02, a10, a11, a12, a20, a21, a22⟩ := rotA.entries392  have square := fifth.square393  apply Orthogonal.of_entries with rotA.matrix394  . rw [a00, a10, a20]395    ring396  . rw [a01, a11, a21]397    rw ← square398    ring399  . rw [a02, a12, a22]400    rw ← square401    ring402  . rw [a00, a01, a10, a11, a20, a21]403    ring404  . rw [a00, a02, a10, a12, a20, a22]405    ring406  . rw [a01, a02, a11, a12, a21, a22]407    ring408  . rw [a00, a01, a02]409    ring410  . rw [a10, a11, a12]411    rw ← square412    ring413  . rw [a20, a21, a22]414    rw ← square415    ring416  . rw [a00, a01, a02, a10, a11, a12]417    ring418  . rw [a00, a01, a02, a20, a21, a22]419    ring420  . rw [a10, a11, a12, a20, a21, a22]421    ring422423theorem rotB.orthogonal424  shows Orthogonal(rotB)425proof426  obtain ⟨b00, b01, b02, b10, b11, b12, b20, b21, b22⟩ := rotB.entries427  have square := fifth.square428  apply Orthogonal.of_entries with rotB.matrix429  . rw [b00, b10, b20]430    rw ← square431    ring432  . rw [b01, b11, b21]433    rw ← square434    ring435  . rw [b02, b12, b22]436    ring437  . rw [b00, b01, b10, b11, b20, b21]438    ring439  . rw [b00, b02, b10, b12, b20, b22]440    ring441  . rw [b01, b02, b11, b12, b21, b22]442    ring443  . rw [b00, b01, b02]444    rw ← square445    ring446  . rw [b10, b11, b12]447    rw ← square448    ring449  . rw [b20, b21, b22]450    ring451  . rw [b00, b01, b02, b10, b11, b12]452    ring453  . rw [b00, b01, b02, b20, b21, b22]454    ring455  . rw [b10, b11, b12, b20, b21, b22]456    ring457458theorem rotA.determinant459  shows determinant3(rotA) = (1:R)460proof461  obtain ⟨a00, a01, a02, a10, a11, a12, a20, a21, a22⟩ := rotA.entries462  have square := fifth.square463  rw determinant3.value464  rw ← square465  rw [a00, a01, a02, a10, a11, a12, a20, a21, a22]466  ring467468theorem rotB.determinant469  shows determinant3(rotB) = (1:R)470proof471  obtain ⟨b00, b01, b02, b10, b11, b12, b20, b21, b22⟩ := rotB.entries472  have square := fifth.square473  rw determinant3.value474  rw ← square475  rw [b00, b01, b02, b10, b11, b12, b20, b21, b22]476  ring477478theorem rotA.so3479  shows rotA ∈ so3Matrices480proof481  exact so3Matrices.mk with rotA.orthogonal, rotA.determinant482483theorem rotB.so3484  shows rotB ∈ so3Matrices485proof486  exact so3Matrices.mk with rotB.orthogonal, rotB.determinant487488theorem rotA.transpose_so3489  shows transpose(rotA) ∈ so3Matrices490proof491  exact so3Matrices.transpose_mem with rotA.so3492493theorem rotB.transpose_so3494  shows transpose(rotB) ∈ so3Matrices495proof496  exact so3Matrices.transpose_mem with rotB.so3497498theorem rotA.inverse499  shows so3Inverse(rotA) = transpose(rotA)500proof501  exact so3Inverse.value with rotA.so3502503theorem rotB.inverse504  shows so3Inverse(rotB) = transpose(rotB)505proof506  exact so3Inverse.value with rotB.so3507508theorem rotA.transpose_mul509  shows Ring.mul(matrixRing(realRing, 3))(transpose(rotA), rotA) =510    Ring.one(matrixRing(realRing, 3))511proof512  exact Orthogonal.left with rotA.orthogonal513514theorem rotA.mul_transpose515  shows Ring.mul(matrixRing(realRing, 3))(rotA, transpose(rotA)) =516    Ring.one(matrixRing(realRing, 3))517proof518  exact Orthogonal.right with rotA.orthogonal519520theorem rotB.transpose_mul521  shows Ring.mul(matrixRing(realRing, 3))(transpose(rotB), rotB) =522    Ring.one(matrixRing(realRing, 3))523proof524  exact Orthogonal.left with rotB.orthogonal525526theorem rotB.mul_transpose527  shows Ring.mul(matrixRing(realRing, 3))(rotB, transpose(rotB)) =528    Ring.one(matrixRing(realRing, 3))529proof530  exact Orthogonal.right with rotB.orthogonal531