OAI/Geometry/Relativity/CKS/RoundCasimir.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSInducedSphere.rotationGenerator_eq line 13
2. lemma OAI.CKSInducedSphere.smoothRotation_pd line 20
3. lemma OAI.CKSInducedSphere.pd_smoothRotation line 25
4. lemma OAI.CKSInducedSphere.smoothRotation_square line 40
5. theorem OAI.CKSInducedSphere.roundLaplacian_eq_Casimir line 50