Planck's constant

In this module we define the Planck's constant ℏ as a positive real number. This is introduced as an axiom.

axiom Constants.ℏ : { x : ℝ // 0 < x }

Planck's constant.

theorem Constants.ℏ_pos : 0 < ↑ℏ

Planck's constant is positive.

theorem Constants.ℏ_nonneg : 0 ≤ ↑ℏ

Planck's constant is non-negative.

theorem Constants.ℏ_ne_zero : ↑ℏ ≠ 0

Planck's constant is not equal to zero.