Momentum

Momentum in d-dimensional space is defined as a d-dimensional vector.

@[reducible, inline]

abbrev Momentum (d : ℕ := 3) : Type

The type Space d representes d dimensional Euclidean space. The default value of d is 3. Thus Space = Space 3.

Equations

• Momentum d = EuclideanSpace ℝ (Fin d)