SphereVolumeOrientation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.sphereFrame_interleaved line 11
Source documentation
The cofactor frame is the actual interleaved real orthonormal coordinate frame, with the same index equivalence used for the volume form.
```
lemma sphereFrame_interleaved (k : ℕ) (s : WedgePowerSlots (k+1)) :
    sphereFrame k (ambientFinEquiv k s) = interleavedBasis s := by
…
```
Mentions: OAI.Mahler.WedgePowerSlots, OAI.Mahler.sphereFrame, OAI.Mahler.ambientFinEquiv, OAI.Mahler.interleavedBasis
theorem OAI.Mahler.sphereVolume_orthonormalFrame line 20
Source documentation
The volume form evaluates to +1 on a real orthonormal frame. This verifies its Euclidean metric normalization as well as its sign.
```
theorem sphereVolume_orthonormalFrame (k : ℕ) : sphereVolume k (sphereFrame k) = 1 := by
…
```
Mentions: OAI.Mahler.sphereVolume, OAI.Mahler.sphereFrame