Physlib.QuantumMechanics.PlanckConstant

Planck's constant

In this module we define the Planck's constant `ℏ` as a positive real number.

4 declarations

definition

Reduced Planck's constant $\hbar$

The reduced Planck's constant $\hbar$ is defined as a positive real number with the value $1.054571817 \times 10^{-34}$ in units of $\text{J} \cdot \text{s}$ .

theorem

$\hbar > 0$

#ℏ_pos

The reduced Planck's constant $\hbar$ is strictly positive, i.e., $0 < \hbar$ .

theorem

$\hbar \ge 0$

#ℏ_nonneg

The reduced Planck's constant $\hbar$ is non-negative, i.e., $0 \le \hbar$ .

theorem

$\hbar \neq 0$

#ℏ_ne_zero

The reduced Planck constant $\hbar$ is not equal to zero, i.e., $\hbar \neq 0$ .

Physlib.QuantumMechanics.PlanckConstant

Planck's constant

Reduced Planck's constant ℏ\hbarℏ

ℏ>0\hbar > 0ℏ>0

ℏ≥0\hbar \ge 0ℏ≥0

ℏ≠0\hbar \neq 0ℏ=0

Reduced Planck's constant $\hbar$

$\hbar > 0$

$\hbar \ge 0$

$\hbar \neq 0$