1. Physlib
  2. QuantumMechanics
  3. PlanckConstant
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Mathlib.Data.NNReal.Defs

Planck's constant

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

@[expose] public section

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

def ℏ : Subtype fun x : ℝ => 0 < x := ⟨1.054571817e-34, ⊢ 0 < 1054571817e-43 All goals completed! 🐙⟩

Planck's constant is positive.

@[simp] lemma ℏ_pos : 0 < (ℏ : ℝ) := ℏ.2

Planck's constant is non-negative.

@[simp] lemma ℏ_nonneg : 0 ≤ (ℏ : ℝ) := le_of_lt ℏ.2

Planck's constant is not equal to zero.

@[simp] lemma ℏ_ne_zero : (ℏ : ℝ) ≠ 0 := ne_of_gt ℏ.2