Physlib

Physlib.QuantumMechanics.PlanckConstant

Planck's constant

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

9 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×10−341.054571817 \times 10^{-34} in units of J⋅s\text{J} \cdot \text{s}.

theorem

ℏ>0\hbar > 0

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

theorem

ℏ≥0\hbar \ge 0

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

theorem

ℏ≠0\hbar \neq 0

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

definition

Planck's constant hh

The Planck constant hh is defined as a positive real number satisfying the relation h=2πℏh = 2\pi\hbar, where ℏ\hbar is the reduced Planck constant.

theorem

h>0h > 0

Planck's constant hh is strictly positive, i.e., h>0h > 0.

theorem

h≥0h \ge 0

The Planck constant hh is non-negative, satisfying the inequality 0≤h0 \le h.

theorem

h≠0h \neq 0

The Planck constant hh is not equal to zero: h≠0h \neq 0.

theorem

h=2πℏh = 2\pi\hbar

The Planck constant hh is equal to 2π2\pi times the reduced Planck constant ℏ\hbar: h=2πℏh = 2\pi\hbar