Skip to content

Commit 00aca87

Browse files
authored
feat: Space slice (#811)
* feat: Create slices for Space Lots of things about distributions here, which may best be seperated. * refactor: Linting * docs: Add documentation * refactor: Lint
1 parent 22c183e commit 00aca87

File tree

3 files changed

+930
-0
lines changed

3 files changed

+930
-0
lines changed

PhysLean.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -323,6 +323,7 @@ import PhysLean.Relativity.Tensors.TensorSpecies.Basic
323323
import PhysLean.Relativity.Tensors.Tensorial
324324
import PhysLean.Relativity.Tensors.UnitTensor
325325
import PhysLean.SpaceAndTime.Space.Basic
326+
import PhysLean.SpaceAndTime.Space.ConstantSliceDist
326327
import PhysLean.SpaceAndTime.Space.CrossProduct
327328
import PhysLean.SpaceAndTime.Space.Derivatives.Basic
328329
import PhysLean.SpaceAndTime.Space.Derivatives.Curl
@@ -335,6 +336,7 @@ import PhysLean.SpaceAndTime.Space.IsDistBounded
335336
import PhysLean.SpaceAndTime.Space.LengthUnit
336337
import PhysLean.SpaceAndTime.Space.Norm
337338
import PhysLean.SpaceAndTime.Space.RadialAngularMeasure
339+
import PhysLean.SpaceAndTime.Space.Slice
338340
import PhysLean.SpaceAndTime.Space.SpaceStruct
339341
import PhysLean.SpaceAndTime.Space.Translations
340342
import PhysLean.SpaceAndTime.SpaceTime.Basic

0 commit comments

Comments
 (0)