Momentum

In this module we define the type Momentum, which represents the momentum of a particle in d-dimensional space, in an arbitrary (but given) set of units.

@[reducible, inline]

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

Momentum in d-dimensional space in an arbitary, but given, set of units. In (3+1)d space time this corresponds to 3-momentum not 4-momentum.

Equations

• Momentum d = Measured (Dimension.M𝓭 * Dimension.L𝓭 * Dimension.T𝓭⁻¹) (Fin d → ℝ)

def Momentum.ofMassAndVelocity {d : ℕ} (m : Mass) (v : Velocity d) : Momentum d

The momentum of a particle with mass m and velocity v.

Equations

• Momentum.ofMassAndVelocity m v = m • v