Documentation Verification Report

Rotations

📁 Source: PhysLean/Relativity/LorentzGroup/Rotations.lean

Statistics

Metric	Count
Definitions `Rotations`, `ofSpecialOrthogonal`	2
Theorems `mem_rotations_iff`, `ofSpecialOrthogonal_continuous`, `ofSpecialOrthogonal_symm_continuous`, `rotations_subset_restricted`, `toVector_rotation`, `transpose_mem_rotations`	6
Total	8

LorentzGroup

Definitions

Name	Category	Theorems
`Rotations` 📖	CompOp	7 math math: `mem_rotations_iff`, `toRotation_continuous`, `ofSpecialOrthogonal_symm_continuous`, `transpose_mem_rotations`, `ofSpecialOrthogonal_continuous`, `toVector_rotation`, `rotations_subset_restricted`
`ofSpecialOrthogonal` 📖	CompOp	2 math math: `ofSpecialOrthogonal_symm_continuous`, `ofSpecialOrthogonal_continuous`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_rotations_iff` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Rotations` `IsProper`	—	—
`ofSpecialOrthogonal_continuous` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Rotations` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `ofSpecialOrthogonal`	—	—
`ofSpecialOrthogonal_symm_continuous` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Rotations` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `ofSpecialOrthogonal`	—	—
`rotations_subset_restricted` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Rotations` `restricted`	—	—
`toVector_rotation` 📖	mathematical	—	`toVector` `LorentzGroup` `lorentzGroupIsGroup` `Rotations` `Lorentz.Vector` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.basis`	—	`toVector_eq_basis_iff_timeComponent_eq_one`
`transpose_mem_rotations` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Rotations` `transpose`	—	—

---

← Back to Index