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	37 math math: QuantumMechanics.HydrogenAtom.angularMomentum_commutation_lrl, QuantumMechanics.OneDimension.positionOperatorSchwartz_momentumOperatorSchwartz_eq, QuantumMechanics.OneDimension.HarmonicOscillator.one_over_ξ, QuantumMechanics.radiusRegPow_commutation_momentumSqr, QuantumMechanics.position_commutation_momentum_momentum, ℏ_pos, QuantumMechanics.OneDimension.momentumOperator_eq_smul, QuantumMechanics.momentum_comp_angularMomentum_eq, QuantumMechanics.angularMomentum_commutation_position, QuantumMechanics.radiusRegPow_commutation_momentum, QuantumMechanics.OneDimension.momentumOperatorSchwartz_positionOperatorSchwartz_eq, QuantumMechanics.angularMomentum_commutation_angularMomentum, QuantumMechanics.HydrogenAtom.lrlOperator_eq'', QuantumMechanics.position_commutation_momentum, ℏ_nonneg, QuantumMechanics.OneDimension.HarmonicOscillator.ξ_inverse, QuantumMechanics.momentum_comp_position_eq, QuantumMechanics.position_commutation_momentumSqr, QuantumMechanics.HydrogenAtom.hamiltonianReg_commutation_lrl, QuantumMechanics.HydrogenAtom.lrl_commutation_lrl, QuantumMechanics.OneDimension.HarmonicOscillator.schrodingerOperator_eq_ξ, QuantumMechanics.HydrogenAtom.lrlOperator_eq', QuantumMechanics.HydrogenAtom.lrlOperatorSqr_eq, QuantumMechanics.OneDimension.HarmonicOscillator.one_over_ξ_sq, QuantumMechanics.position_position_commutation_momentum, QuantumMechanics.OneDimension.planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded, QuantumMechanics.OneDimension.momentumOperatorSchwartz_apply, QuantumMechanics.momentumOperator_apply, QuantumMechanics.HydrogenAtom.lrlOperator_eq, QuantumMechanics.momentumOperator_apply_fun, QuantumMechanics.OneDimension.HarmonicOscillator.m_mul_ω_div_two_ℏ_pos, QuantumMechanics.OneDimension.HarmonicOscillator.ξ_sq, QuantumMechanics.momentum_comp_radiusRegPow_eq, 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