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
The reduced Planck's constant is defined as a positive real number with the value in units of .
theorem
The reduced Planck's constant is strictly positive, i.e., .
theorem
The reduced Planck's constant is non-negative, i.e., .
theorem
The reduced Planck constant is not equal to zero, i.e., .
definition
Planck's constant
The Planck constant is defined as a positive real number satisfying the relation , where is the reduced Planck constant.
theorem
Planck's constant is strictly positive, i.e., .
theorem
The Planck constant is non-negative, satisfying the inequality .
theorem
The Planck constant is not equal to zero: .
theorem
The Planck constant is equal to times the reduced Planck constant :
