Pith. sign in

Geometry

Geometry modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.

38 modules · 622 thm/lemma · 15044 lines
module thm lemma def lines papers
Geometry.AffineIndepInterior 24 0 3 500 -
Geometry.CayleyMenger 5 0 3 229 -
Geometry.CayleyMengerDerivatives 17 0 15 368 -
Geometry.CayleyMengerMatrix 30 0 12 344 -
Geometry.CayleyMengerN 1 0 4 69 -
Geometry.CayleyMengerPolynomial 7 0 3 203 -
Geometry.CofactorDerivatives 20 0 14 422 -
Geometry.CofactorPolynomial 86 0 30 1078 -
Geometry.DeficitLinearization 2 0 1 196 -
Geometry.DihedralAngle 10 0 5 184 -
Geometry.DihedralCayleyMenger 5 0 8 147 -
Geometry.DihedralCofactorFormula 72 0 8 874 -
Geometry.DihedralDerivatives 7 0 2 185 -
Geometry.DiscreteBianchi 6 0 5 253 -
Geometry.FreudenthalCubeTriangulation 5 0 11 286 -
Geometry.FreudenthalReggeComponent 11 0 7 213 -
Geometry.FreudenthalTwoCubeStrip 4 0 9 310 -
Geometry.GramCayleyMenger 8 0 3 130 -
Geometry.PeriodicFreudenthalTorus 25 0 30 729 -
Geometry.RealisabilityCone 2 0 1 60 -
Geometry.ReggeActionConcrete 21 0 22 677 -
Geometry.ReggeActionCubicTaylorBound 37 0 16 1186 -
Geometry.ReggeActionFirstVariation 29 0 26 1203 -
Geometry.ReggeActionNonlinearCorrespondence 14 0 5 212 -
Geometry.ReggeActionNonlinearHessianProof 88 0 54 2372 -
Geometry.ReggeActionSecondVariation 6 0 9 193 -
Geometry.ReggeActionSmoothness 24 0 3 372 -
Geometry.ReggeHessian3D 2 0 2 66 -
Geometry.ReggeRemainderClosureAudit 5 0 1 101 -
Geometry.ReggeRigorousFoundation 4 0 5 343 -
Geometry.ReggeTriangulation3D 0 0 0 41 -
Geometry.Schlaefli 4 0 4 193 -
Geometry.SchlaefliN 1 0 1 47 -
Geometry.SchlaefliTetrahedron 4 0 4 122 -
Geometry.SchlaefliTetrahedronProof 26 0 19 850 -
Geometry.SchlaefliTriangulation3D 1 0 2 60 -
Geometry.TetrahedronRealization 3 0 9 96 -
Geometry.Triangulation3DConsistency 6 0 3 130 -

full source mirrored from github.com/jonwashburn/shape-of-logic