PhyslibSearch

theorem

Extensionality of physical dimensions: $d_1 = d_2$ if all base components are equal

For any two physical dimensions $d_1$ and $d_2$ , if their base components for length, time, mass, charge, and temperature are respectively equal—that is, $d_1.\text{length} = d_2.\text{length}$ , $d_1.\text{time} = d_2.\text{time}$ , $d_1.\text{mass} = d_2.\text{mass}$ , $d_1.\text{charge} = d_2.\text{charge}$ , and $d_1.\text{temperature} = d_2.\text{temperature}$ —then the dimensions are equal, $d_1 = d_2$ .

instance

Multiplication of physical dimensions $d_1 \cdot d_2$

#instMul

For any two physical dimensions $d_1, d_2 \in \text{Dimension}$ , their product $d_1 \cdot d_2$ is defined as the dimension whose base component exponents are the sums of the corresponding exponents in $d_1$ and $d_2$ . Specifically: - $(d_1 \cdot d_2).\text{length} = d_1.\text{length} + d_2.\text{length}$ - $(d_1 \cdot d_2).\text{time} = d_1.\text{time} + d_2.\text{time}$ - $(d_1 \cdot d_2).\text{mass} = d_1.\text{mass} + d_2.\text{mass}$ - $(d_1 \cdot d_2).\text{charge} = d_1.\text{charge} + d_2.\text{charge}$ - $(d_1 \cdot d_2).\text{temperature} = d_1.\text{temperature} + d_2.\text{temperature}$

theorem

$(d_1 \cdot d_2).\text{time} = d_1.\text{time} + d_2.\text{time}$

#time_mul

For any two physical dimensions $d_1$ and $d_2$ , the exponent of the time component in their product $d_1 \cdot d_2$ is equal to the sum of the time exponents of $d_1$ and $d_2$ . That is, $(d_1 \cdot d_2).\text{time} = d_1.\text{time} + d_2.\text{time}$ .

theorem

$(d_1 \cdot d_2).\text{length} = d_1.\text{length} + d_2.\text{length}$

#length_mul

For any two physical dimensions $d_1$ and $d_2$ , the exponent of the length component in their product $d_1 \cdot d_2$ is equal to the sum of the length exponents of $d_1$ and $d_2$ . That is, $(d_1 \cdot d_2).\text{length} = d_1.\text{length} + d_2.\text{length}$ .

theorem

$(d_1 \cdot d_2).\text{mass} = d_1.\text{mass} + d_2.\text{mass}$

#mass_mul

For any two physical dimensions $d_1$ and $d_2$ , the exponent of the mass component in their product $d_1 \cdot d_2$ is equal to the sum of the mass exponents of $d_1$ and $d_2$ . That is, $(d_1 \cdot d_2).\text{mass} = d_1.\text{mass} + d_2.\text{mass}$ .

theorem

$(d_1 \cdot d_2).\text{charge} = d_1.\text{charge} + d_2.\text{charge}$

#charge_mul

For any two physical dimensions $d_1$ and $d_2$ , the exponent of the charge component in their product $d_1 \cdot d_2$ is equal to the sum of the charge exponents of $d_1$ and $d_2$ . That is, $(d_1 \cdot d_2).\text{charge} = d_1.\text{charge} + d_2.\text{charge}$ .

theorem

$(d_1 \cdot d_2).\text{temperature} = d_1.\text{temperature} + d_2.\text{temperature}$

#temperature_mul

For any two physical dimensions $d_1$ and $d_2$ , the temperature component of their product $d_1 \cdot d_2$ is equal to the sum of the temperature components of $d_1$ and $d_2$ . This is expressed as $(d_1 \cdot d_2).\text{temperature} = d_1.\text{temperature} + d_2.\text{temperature}$ .

instance

Dimensionless identity $1$

#instOne

The multiplicative identity element $1$ of the type `Dimension` is defined as the dimension where all five base components (exponents) are zero, representing a dimensionless quantity. Mathematically, it is given by the 5-tuple $\langle 0, 0, 0, 0, 0 \rangle$ .

theorem

$1.\text{length} = 0$

#one_length

The length component of the dimensionless identity $1$ in the type $\text{Dimension}$ is $0$ , which is expressed as $1.\text{length} = 0$ .

theorem

$1.\text{time} = 0$

#one_time

The time component of the dimensionless identity $1$ in the type $\text{Dimension}$ is $0$ , which is expressed as $1.\text{time} = 0$ .

theorem

$1.\text{mass} = 0$

#one_mass

The mass component of the dimensionless identity $1 \in \text{Dimension}$ is equal to $0$ .

theorem

The charge component of $1$ is $0$

#one_charge

The charge component of the dimensionless identity $1 \in \text{Dimension}$ is equal to $0$ .

theorem

The temperature component of $1$ is $0$

#one_temperature

The temperature component of the dimensionless identity $1 \in \text{Dimension}$ is equal to $0$ .

instance

$\text{Dimension}$ forms a commutative group

#instCommGroup

The type `Dimension` of physical dimensions forms a commutative group (abelian group) under the multiplication operation. In this group, the product of two dimensions corresponds to the component-wise addition of their base exponents (length, time, mass, charge, and temperature). The identity element $1$ represents the dimensionless quantity where all base exponents are zero, and the inverse $d^{-1}$ is obtained by negating each base exponent of the dimension $d$ .

theorem

The length component of $d^{-1}$ is $-d.\text{length}$

#inv_length

For any physical dimension $d$ , the length component of its inverse $d^{-1}$ is equal to the negative of the length component of $d$ , that is, $(d^{-1}).\text{length} = -d.\text{length}$ .

theorem

The time component of $d^{-1}$ is $-d.\text{time}$

#inv_time

For any physical dimension $d$ , the time component (the exponent of the time base unit) of its group inverse $d^{-1}$ is equal to the negation of the time component of $d$ . This is expressed as: $(d^{-1}).\text{time} = -d.\text{time}$ where the inverse $d^{-1}$ is the element in the commutative group of dimensions such that $d \cdot d^{-1} = 1$ .

theorem

$(d^{-1}).\text{mass} = -d.\text{mass}$

#inv_mass

For any physical dimension $d$ , the mass exponent of its inverse dimension $d^{-1}$ is equal to the negation of the mass exponent of $d$ , i.e., $(d^{-1}).\text{mass} = -(d.\text{mass})$ .

theorem

$(d^{-1}).\text{charge} = -(d.\text{charge})$

#inv_charge

For any physical dimension $d$ , the charge component of its inverse $d^{-1}$ is equal to the negative of its charge component, i.e., $(d^{-1}).\text{charge} = -(d.\text{charge})$ .

theorem

$(d^{-1}).\text{temperature} = -d.\text{temperature}$

#inv_temperature

For any physical dimension $d$ , the temperature component of its inverse $d^{-1}$ is equal to the negative of the temperature component of $d$ , expressed as $(d^{-1}).\text{temperature} = -d.\text{temperature}$ .

theorem

$(d_1 / d_2).\text{length} = d_1.\text{length} - d_2.\text{length}$

#div_length

For any two physical dimensions $d_1$ and $d_2$ , the exponent of the length component in their quotient $d_1 / d_2$ is equal to the difference between the length exponents of $d_1$ and $d_2$ . That is, $(d_1 / d_2).\text{length} = d_1.\text{length} - d_2.\text{length}$ .

theorem

$(d_1 / d_2).\text{time} = d_1.\text{time} - d_2.\text{time}$

#div_time

For any two physical dimensions $d_1$ and $d_2$ , the time component (the exponent of the time base unit) of their quotient $d_1 / d_2$ is equal to the difference between the time components of $d_1$ and $d_2$ . This is expressed as: $(d_1 / d_2).\text{time} = d_1.\text{time} - d_2.\text{time}$

theorem

$(d_1 / d_2).\text{mass} = d_1.\text{mass} - d_2.\text{mass}$

#div_mass

For any two physical dimensions $d_1$ and $d_2$ , the mass exponent of the quotient $d_1 / d_2$ is equal to the difference between the mass exponent of $d_1$ and the mass exponent of $d_2$ , i.e., $(d_1 / d_2).\text{mass} = d_1.\text{mass} - d_2.\text{mass}$ .

theorem

$(d_1 / d_2).\text{charge} = d_1.\text{charge} - d_2.\text{charge}$

#div_charge

For any two physical dimensions $d_1$ and $d_2$ , the charge component of their quotient $d_1 / d_2$ is equal to the difference of the charge components of $d_1$ and $d_2$ . That is, $(d_1 / d_2).\text{charge} = d_1.\text{charge} - d_2.\text{charge}$ .

theorem

$(d_1 / d_2).\text{temperature} = d_1.\text{temperature} - d_2.\text{temperature}$

#div_temperature

For any two physical dimensions $d_1, d_2 \in \text{Dimension}$ , the temperature component of their quotient $d_1 / d_2$ is equal to the difference between the temperature component of $d_1$ and the temperature component of $d_2$ . That is, $(d_1 / d_2).\text{temperature} = d_1.\text{temperature} - d_2.\text{temperature}$ .

theorem

$(d^n).\text{length} = n \cdot d.\text{length}$

#npow_length

For any physical dimension $d$ and any natural number $n$ , the length component of the $n$ -th power of the dimension $d$ is equal to $n$ times the length component of $d$ . That is, $(d^n).\text{length} = n \cdot d.\text{length}$ .

theorem

$(d^n).\text{time} = n \cdot d.\text{time}$

#npow_time

For any physical dimension $d$ and any natural number $n$ , the time component (exponent) of the dimension $d^n$ is equal to $n$ times the time component of $d$ . That is, $(d^n)_{\text{time}} = n \cdot d_{\text{time}}$ .

theorem

$\text{mass}(d^n) = n \cdot \text{mass}(d)$

#npow_mass

For any physical dimension $d$ and any natural number $n$ , the mass component of the dimension $d^n$ is equal to $n$ times the mass component of $d$ . Mathematically, this is expressed as: $(d^n)_{\text{mass}} = n \cdot d_{\text{mass}}$ where $d^n$ denotes the $n$ -th power of the dimension in the commutative group of dimensions, and the mass component represents the exponent of the base mass dimension.

theorem

$(d^n).\text{charge} = n \cdot d.\text{charge}$

#npow_charge

For any physical dimension $d$ and any natural number $n$ , the charge component of the dimension $d^n$ is equal to $n$ times the charge component of $d$ . Here, the charge component represents the exponent of the base charge dimension.

theorem

$(d^n)_{\text{temp}} = n \cdot d_{\text{temp}}$ for $n \in \mathbb{N}$

#npow_temperature

For any physical dimension $d$ and any natural number $n$ , the temperature component of the dimension $d^n$ is equal to $n$ times the temperature component of $d$ , which can be expressed as $(d^n)_{\text{temp}} = n \cdot d_{\text{temp}}$ .

instance

Rational power of a dimension $d^n$ for $n \in \mathbb{Q}$

#instPowRat

For a physical dimension $d$ and a rational number $n \in \mathbb{Q}$ , the power operation $d^n$ is defined as the dimension whose fundamental components—length, time, mass, charge, and temperature—are obtained by multiplying the corresponding components of $d$ by $n$ .

definition

Dimension of length $L_{\mathfrak{d}}$

#L𝓭

The constant $L_{\mathfrak{d}}$ represents the physical dimension of length. In the representation of dimensions as a vector of exponents for base quantities, it corresponds to the tuple $(1, 0, 0, 0, 0)$ , where the component for length is $1$ and all other base dimensions (such as time, mass, etc.) are $0$ .

theorem

The length component of $L_{\mathfrak{d}}$ is $1$

#L𝓭_length

The length component of the physical dimension of length $L_{\mathfrak{d}}$ is equal to $1$ .

theorem

Time component of $L_{\mathfrak{d}}$ is $0$

#L𝓭_time

The time component of the dimension of length $L_{\mathfrak{d}}$ is equal to $0$ .

theorem

The mass component of $L_{\mathfrak{d}}$ is $0$

#L𝓭_mass

The mass component of the physical dimension of length $L_{\mathfrak{d}}$ is equal to $0$ .

theorem

The charge component of $L_{\mathfrak{d}}$ is $0$

#L𝓭_charge

The charge component of the physical dimension of length $L_{\mathfrak{d}}$ is equal to $0$ .

theorem

The temperature component of $L_{\mathfrak{d}}$ is $0$

#L𝓭_temperature

The temperature component of the physical dimension of length $L_{\mathfrak{d}}$ is $0$ .

definition

Dimension of time

#T𝓭

The base physical dimension for time, typically denoted as $[T]$ or $T$ . In the vector representation of physical dimensions, it corresponds to an exponent of $1$ for the time component and $0$ for all other base dimensions (such as length, mass, electric current, and temperature).

theorem

The length component of $T_{\mathfrak{d}}$ is $0$

#T𝓭_length

The length component of the physical dimension of time, denoted as $T_{\mathfrak{d}}$ , is $0$ .

theorem

The time component of $T_{\mathfrak{d}}$ is $1$

#T𝓭_time

For the base physical dimension of time, denoted as $T_{\mathfrak{d}}$ , the time component (or exponent) is $1$ .

theorem

The mass component of the dimension of time is $0$

#T𝓭_mass

For the base physical dimension of time, denoted as $T$ , the mass component (or mass exponent) is $0$ .

theorem

The charge component of the dimension of time is $0$

#T𝓭_charge

For the base physical dimension of time, denoted as $T$ , the electric charge component (or exponent) is $0$ .

theorem

The temperature component of the dimension of time is $0$

#T𝓭_temperature

For the base physical dimension of time, denoted as $T$ , the temperature component (or temperature exponent) is $0$ .

definition

Dimension of mass ( $\mathsf{M}$ )

#M𝓭

The constant `Dimension.M𝓭` represents the base physical dimension of mass, denoted as $\mathsf{M}$ . In the system of base dimensions, it is defined by the vector $\langle 0, 0, 1, 0, 0 \rangle$ , where the third component corresponds to the exponent of the mass dimension and all other base dimensions (such as length, time, electric charge, and temperature) are zero.

definition

Dimension of electric charge ( $\mathsf{Q}$ )

#C𝓭

The constant `Dimension.C𝓭` represents the base physical dimension of electric charge, denoted as $\mathsf{Q}$ . In the system of base dimensions, it is defined by the vector $\langle 0, 0, 0, 1, 0 \rangle$ , where the fourth component corresponds to the exponent of the charge dimension and all other base dimensions (such as length, mass, and time) are zero.

definition

Dimension of temperature $\Theta$

#Θ𝓭

The constant $\Theta_d$ represents the base physical dimension of thermodynamic temperature. In the representation of dimensions as a vector of exponents, it corresponds to the vector $\langle 0, 0, 0, 0, 1 \rangle$ , where the fifth component (temperature) is unit and all other base dimensions are zero.

Physlib.Units.Dimension

Extensionality of physical dimensions: d1=d2d_1 = d_2d1​=d2​ if all base components are equal

Multiplication of physical dimensions d1⋅d2d_1 \cdot d_2d1​⋅d2​

(d1⋅d2).time=d1.time+d2.time(d_1 \cdot d_2).\text{time} = d_1.\text{time} + d_2.\text{time}(d1​⋅d2​).time=d1​.time+d2​.time

(d1⋅d2).length=d1.length+d2.length(d_1 \cdot d_2).\text{length} = d_1.\text{length} + d_2.\text{length}(d1​⋅d2​).length=d1​.length+d2​.length

(d1⋅d2).mass=d1.mass+d2.mass(d_1 \cdot d_2).\text{mass} = d_1.\text{mass} + d_2.\text{mass}(d1​⋅d2​).mass=d1​.mass+d2​.mass

(d1⋅d2).charge=d1.charge+d2.charge(d_1 \cdot d_2).\text{charge} = d_1.\text{charge} + d_2.\text{charge}(d1​⋅d2​).charge=d1​.charge+d2​.charge

(d1⋅d2).temperature=d1.temperature+d2.temperature(d_1 \cdot d_2).\text{temperature} = d_1.\text{temperature} + d_2.\text{temperature}(d1​⋅d2​).temperature=d1​.temperature+d2​.temperature

Dimensionless identity 111

1.length=01.\text{length} = 01.length=0

1.time=01.\text{time} = 01.time=0

1.mass=01.\text{mass} = 01.mass=0

The charge component of 111 is 000

The temperature component of 111 is 000

Dimension\text{Dimension}Dimension forms a commutative group

The length component of d−1d^{-1}d−1 is −d.length-d.\text{length}−d.length

The time component of d−1d^{-1}d−1 is −d.time-d.\text{time}−d.time

(d−1).mass=−d.mass(d^{-1}).\text{mass} = -d.\text{mass}(d−1).mass=−d.mass

(d−1).charge=−(d.charge)(d^{-1}).\text{charge} = -(d.\text{charge})(d−1).charge=−(d.charge)

(d−1).temperature=−d.temperature(d^{-1}).\text{temperature} = -d.\text{temperature}(d−1).temperature=−d.temperature

(d1/d2).length=d1.length−d2.length(d_1 / d_2).\text{length} = d_1.\text{length} - d_2.\text{length}(d1​/d2​).length=d1​.length−d2​.length

(d1/d2).time=d1.time−d2.time(d_1 / d_2).\text{time} = d_1.\text{time} - d_2.\text{time}(d1​/d2​).time=d1​.time−d2​.time

(d1/d2).mass=d1.mass−d2.mass(d_1 / d_2).\text{mass} = d_1.\text{mass} - d_2.\text{mass}(d1​/d2​).mass=d1​.mass−d2​.mass

(d1/d2).charge=d1.charge−d2.charge(d_1 / d_2).\text{charge} = d_1.\text{charge} - d_2.\text{charge}(d1​/d2​).charge=d1​.charge−d2​.charge

(d1/d2).temperature=d1.temperature−d2.temperature(d_1 / d_2).\text{temperature} = d_1.\text{temperature} - d_2.\text{temperature}(d1​/d2​).temperature=d1​.temperature−d2​.temperature

(dn).length=n⋅d.length(d^n).\text{length} = n \cdot d.\text{length}(dn).length=n⋅d.length

(dn).time=n⋅d.time(d^n).\text{time} = n \cdot d.\text{time}(dn).time=n⋅d.time

mass(dn)=n⋅mass(d)\text{mass}(d^n) = n \cdot \text{mass}(d)mass(dn)=n⋅mass(d)

(dn).charge=n⋅d.charge(d^n).\text{charge} = n \cdot d.\text{charge}(dn).charge=n⋅d.charge

(dn)temp=n⋅dtemp(d^n)_{\text{temp}} = n \cdot d_{\text{temp}}(dn)temp​=n⋅dtemp​ for n∈Nn \in \mathbb{N}n∈N

Rational power of a dimension dnd^ndn for n∈Qn \in \mathbb{Q}n∈Q

Dimension of length LdL_{\mathfrak{d}}Ld​

The length component of LdL_{\mathfrak{d}}Ld​ is 111

Time component of LdL_{\mathfrak{d}}Ld​ is 000

The mass component of LdL_{\mathfrak{d}}Ld​ is 000

The charge component of LdL_{\mathfrak{d}}Ld​ is 000

The temperature component of LdL_{\mathfrak{d}}Ld​ is 000

Dimension of time

The length component of TdT_{\mathfrak{d}}Td​ is 000

The time component of TdT_{\mathfrak{d}}Td​ is 111

The mass component of the dimension of time is 000

The charge component of the dimension of time is 000

The temperature component of the dimension of time is 000

Dimension of mass (M\mathsf{M}M)

Dimension of electric charge (Q\mathsf{Q}Q)

Dimension of temperature Θ\ThetaΘ

Extensionality of physical dimensions: $d_1 = d_2$ if all base components are equal

Multiplication of physical dimensions $d_1 \cdot d_2$

$(d_1 \cdot d_2).\text{time} = d_1.\text{time} + d_2.\text{time}$

$(d_1 \cdot d_2).\text{length} = d_1.\text{length} + d_2.\text{length}$

$(d_1 \cdot d_2).\text{mass} = d_1.\text{mass} + d_2.\text{mass}$

$(d_1 \cdot d_2).\text{charge} = d_1.\text{charge} + d_2.\text{charge}$

$(d_1 \cdot d_2).\text{temperature} = d_1.\text{temperature} + d_2.\text{temperature}$

Dimensionless identity $1$

$1.\text{length} = 0$

$1.\text{time} = 0$

$1.\text{mass} = 0$

The charge component of $1$ is $0$

The temperature component of $1$ is $0$

$\text{Dimension}$ forms a commutative group

The length component of $d^{-1}$ is $-d.\text{length}$

The time component of $d^{-1}$ is $-d.\text{time}$

$(d^{-1}).\text{mass} = -d.\text{mass}$

$(d^{-1}).\text{charge} = -(d.\text{charge})$

$(d^{-1}).\text{temperature} = -d.\text{temperature}$

$(d_1 / d_2).\text{length} = d_1.\text{length} - d_2.\text{length}$

$(d_1 / d_2).\text{time} = d_1.\text{time} - d_2.\text{time}$

$(d_1 / d_2).\text{mass} = d_1.\text{mass} - d_2.\text{mass}$

$(d_1 / d_2).\text{charge} = d_1.\text{charge} - d_2.\text{charge}$

$(d_1 / d_2).\text{temperature} = d_1.\text{temperature} - d_2.\text{temperature}$

$(d^n).\text{length} = n \cdot d.\text{length}$

$(d^n).\text{time} = n \cdot d.\text{time}$

$\text{mass}(d^n) = n \cdot \text{mass}(d)$

$(d^n).\text{charge} = n \cdot d.\text{charge}$

$(d^n)_{\text{temp}} = n \cdot d_{\text{temp}}$ for $n \in \mathbb{N}$

Rational power of a dimension $d^n$ for $n \in \mathbb{Q}$

Dimension of length $L_{\mathfrak{d}}$

The length component of $L_{\mathfrak{d}}$ is $1$

Time component of $L_{\mathfrak{d}}$ is $0$

The mass component of $L_{\mathfrak{d}}$ is $0$

The charge component of $L_{\mathfrak{d}}$ is $0$

The temperature component of $L_{\mathfrak{d}}$ is $0$

The length component of $T_{\mathfrak{d}}$ is $0$

The time component of $T_{\mathfrak{d}}$ is $1$

The mass component of the dimension of time is $0$

The charge component of the dimension of time is $0$

The temperature component of the dimension of time is $0$

Dimension of mass ( $\mathsf{M}$ )

Dimension of electric charge ( $\mathsf{Q}$ )

Dimension of temperature $\Theta$