Skip to content

Commit 8588dc3

Browse files
committed
feat(Geometry/Euclidean): volume of a simplex
1 parent d507354 commit 8588dc3

3 files changed

Lines changed: 760 additions & 0 deletions

File tree

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4310,6 +4310,7 @@ public import Mathlib.Geometry.Euclidean.Sphere.Ptolemy
43104310
public import Mathlib.Geometry.Euclidean.Sphere.SecondInter
43114311
public import Mathlib.Geometry.Euclidean.Sphere.Tangent
43124312
public import Mathlib.Geometry.Euclidean.Triangle
4313+
public import Mathlib.Geometry.Euclidean.Volume.Integral
43134314
public import Mathlib.Geometry.Euclidean.Volume.Measure
43144315
public import Mathlib.Geometry.Group.Growth.LinearLowerBound
43154316
public import Mathlib.Geometry.Group.Growth.QuotientInter

0 commit comments

Comments
 (0)