Planck's constant

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

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

The value of the reduced Planck's constant in units of J.s.

Equations

• Constants.ℏ = ⟨1054571817e-43, Constants.ℏ._proof_1⟩

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.