Dimension #

In this module we define the type Dimension which carries the dimension of a physical quantity.

Defining dimensions #

source

structure Dimension :

Type

The foundational dimensions. Defined in the order ⟨length, time, mass, charge, temperature⟩

length : ℚ
The length dimension.
time : ℚ
The time dimension.
mass : ℚ
The mass dimension.
charge : ℚ
The charge dimension.
temperature : ℚ
The temperature dimension.

Instances For

source

theorem Dimension.ext {d1 d2 : Dimension} (h1 : d1.length = d2.length) (h2 : d1.time = d2.time) (h3 : d1.mass = d2.mass) (h4 : d1.charge = d2.charge) (h5 : d1.temperature = d2.temperature) :

d1 = d2

source

theorem Dimension.ext_iff {d1 d2 : Dimension} :

d1 = d2 ↔ d1.length = d2.length ∧ d1.time = d2.time ∧ d1.mass = d2.mass ∧ d1.charge = d2.charge ∧ d1.temperature = d2.temperature

source

instance Dimension.instMul :

Mul Dimension

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem Dimension.time_mul (d1 d2 : Dimension) :

(d1 * d2).time = d1.time + d2.time

source

@[simp]

theorem Dimension.length_mul (d1 d2 : Dimension) :

(d1 * d2).length = d1.length + d2.length

source

@[simp]

theorem Dimension.mass_mul (d1 d2 : Dimension) :

(d1 * d2).mass = d1.mass + d2.mass

source

@[simp]

theorem Dimension.charge_mul (d1 d2 : Dimension) :

(d1 * d2).charge = d1.charge + d2.charge

source

@[simp]

theorem Dimension.temperature_mul (d1 d2 : Dimension) :

(d1 * d2).temperature = d1.temperature + d2.temperature

source

instance Dimension.instOne :

One Dimension

Equations

Dimension.instOne = { one := { length := 0, time := 0, mass := 0, charge := 0, temperature := 0 } }

source

@[simp]

theorem Dimension.one_length :

length 1 = 0

source

@[simp]

theorem Dimension.one_time :

time 1 = 0

source

@[simp]

theorem Dimension.one_mass :

mass 1 = 0

source

@[simp]

theorem Dimension.one_charge :

charge 1 = 0

source

@[simp]

theorem Dimension.one_temperature :

temperature 1 = 0

source

instance Dimension.instCommGroup :

CommGroup Dimension

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem Dimension.inv_length (d : Dimension) :

d⁻¹.length = -d.length

source

@[simp]

theorem Dimension.inv_time (d : Dimension) :

d⁻¹.time = -d.time

source

@[simp]

theorem Dimension.inv_mass (d : Dimension) :

d⁻¹.mass = -d.mass

source

@[simp]

theorem Dimension.inv_charge (d : Dimension) :

d⁻¹.charge = -d.charge

source

@[simp]

theorem Dimension.inv_temperature (d : Dimension) :

d⁻¹.temperature = -d.temperature

source

@[simp]

theorem Dimension.div_length (d1 d2 : Dimension) :

(d1 / d2).length = d1.length - d2.length

source

@[simp]

theorem Dimension.div_time (d1 d2 : Dimension) :

(d1 / d2).time = d1.time - d2.time

source

@[simp]

theorem Dimension.div_mass (d1 d2 : Dimension) :

(d1 / d2).mass = d1.mass - d2.mass

source

@[simp]

theorem Dimension.div_charge (d1 d2 : Dimension) :

(d1 / d2).charge = d1.charge - d2.charge

source

@[simp]

theorem Dimension.div_temperature (d1 d2 : Dimension) :

(d1 / d2).temperature = d1.temperature - d2.temperature

source

@[simp]

theorem Dimension.npow_length (d : Dimension) (n : ℕ) :

(d ^ n).length = n • d.length

source

@[simp]

theorem Dimension.npow_time (d : Dimension) (n : ℕ) :

(d ^ n).time = n • d.time

source

@[simp]

theorem Dimension.npow_mass (d : Dimension) (n : ℕ) :

(d ^ n).mass = n • d.mass

source

@[simp]

theorem Dimension.npow_charge (d : Dimension) (n : ℕ) :

(d ^ n).charge = n • d.charge

source

@[simp]

theorem Dimension.npow_temperature (d : Dimension) (n : ℕ) :

(d ^ n).temperature = n • d.temperature

source

instance Dimension.instPowRat :

Pow Dimension ℚ

Equations

One or more equations did not get rendered due to their size.

source

def Dimension.L𝓭 :

Dimension

The dimension corresponding to length.

Equations

Dimension.L𝓭 = { length := 1, time := 0, mass := 0, charge := 0, temperature := 0 }

Instances For

source

@[simp]

theorem Dimension.L𝓭_length :

L𝓭.length = 1

source

@[simp]

theorem Dimension.L𝓭_time :

L𝓭.time = 0

source

@[simp]

theorem Dimension.L𝓭_mass :

L𝓭.mass = 0

source

@[simp]

theorem Dimension.L𝓭_charge :

L𝓭.charge = 0

source

@[simp]

theorem Dimension.L𝓭_temperature :

L𝓭.temperature = 0

source

def Dimension.T𝓭 :

Dimension

The dimension corresponding to time.

Equations

Dimension.T𝓭 = { length := 0, time := 1, mass := 0, charge := 0, temperature := 0 }

Instances For

source

@[simp]

theorem Dimension.T𝓭_length :

T𝓭.length = 0

source

@[simp]

theorem Dimension.T𝓭_time :

T𝓭.time = 1

source

@[simp]

theorem Dimension.T𝓭_mass :

T𝓭.mass = 0

source

@[simp]

theorem Dimension.T𝓭_charge :

T𝓭.charge = 0

source

@[simp]

theorem Dimension.T𝓭_temperature :

T𝓭.temperature = 0

source

def Dimension.M𝓭 :

Dimension

The dimension corresponding to mass.

Equations

Dimension.M𝓭 = { length := 0, time := 0, mass := 1, charge := 0, temperature := 0 }

Instances For

source

def Dimension.C𝓭 :

Dimension

The dimension corresponding to charge.

Equations

Dimension.C𝓭 = { length := 0, time := 0, mass := 0, charge := 1, temperature := 0 }

Instances For

source

def Dimension.Θ𝓭 :

Dimension

The dimension corresponding to temperature.

Equations

Dimension.Θ𝓭 = { length := 0, time := 0, mass := 0, charge := 0, temperature := 1 }

Instances For

PhysLean Documentation

PhysLean.Units.Dimension

Dimension #

Defining dimensions #