OAI/RepresentationTheory/VertexAlgebra/MobiusGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StronglyRationalVOA.CircleMobiusGeometry.Rel line 11
2. def OAI.StronglyRationalVOA.CircleMobiusGeometry.Implements line 14
3. def OAI.StronglyRationalVOA.CircleMobiusGeometry.density line 16
4. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.det line 19
5. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.cos_sq_add_sin_sq line 21
6. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.collinear_unit line 23
7. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.derivative_density line 29
8. def OAI.StronglyRationalVOA.CircleMobiusGeometry.constant line 84
9. def OAI.StronglyRationalVOA.CircleMobiusGeometry.cosine line 85
10. def OAI.StronglyRationalVOA.CircleMobiusGeometry.sine line 86
11. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.density_trigonometric line 87
12. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.determinant_constants line 99
13. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.push_constant line 103