PlanckConstant

📁 Source: PhysLean/QuantumMechanics/PlanckConstant.lean

Statistics

Metric	Count
Definitions ℏ	1
Theorems ℏ_ne_zero, ℏ_nonneg, ℏ_pos	3
Total	4

Constants

Definitions

Name	Category	Theorems
ℏ 📖	CompOp	22 math math: QuantumMechanics.OneDimension.positionOperatorSchwartz_momentumOperatorSchwartz_eq, QuantumMechanics.OneDimension.HarmonicOscillator.one_over_ξ, ℏ_pos, QuantumMechanics.OneDimension.momentumOperator_eq_smul, QuantumMechanics.angularMomentum_commutation_position, QuantumMechanics.OneDimension.momentumOperatorSchwartz_positionOperatorSchwartz_eq, QuantumMechanics.angularMomentum_commutation_angularMomentum, QuantumMechanics.position_commutation_momentum, ℏ_nonneg, QuantumMechanics.OneDimension.HarmonicOscillator.ξ_inverse, QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eq_ξ, QuantumMechanics.OneDimension.HarmonicOscillator.one_over_ξ_sq, QuantumMechanics.OneDimension.planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded, QuantumMechanics.OneDimension.momentumOperatorSchwartz_apply, QuantumMechanics.momentumOperator_apply, QuantumMechanics.momentumOperator_apply_fun, QuantumMechanics.OneDimension.HarmonicOscillator.m_mul_ω_div_two_ℏ_pos, QuantumMechanics.OneDimension.HarmonicOscillator.ξ_sq, QuantumMechanics.angularMomentum_commutation_momentum, QuantumMechanics.OneDimension.positionOperatorSchwartz_commutation_momentumOperatorSchwartz, QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eq, QuantumMechanics.OneDimension.HarmonicOscillator.m_mul_ω_div_ℏ_pos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ℏ_ne_zero 📖	—	—	—	—	—
ℏ_nonneg 📖	mathematical	—	ℏ	—	—
ℏ_pos 📖	mathematical	—	ℏ	—	—

---

← Back to Index