Commutation

📁 Source: PhysLean/QuantumMechanics/OneDimension/Operators/Commutation.lean

Statistics

Metric	Count
Definitions	0
Theorems momentumOperatorSchwartz_positionOperatorSchwartz_eq, positionOperatorSchwartz_commutation_momentumOperatorSchwartz, positionOperatorSchwartz_momentumOperatorSchwartz_eq	3
Total	3

QuantumMechanics.OneDimension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
momentumOperatorSchwartz_positionOperatorSchwartz_eq 📖	mathematical	—	momentumOperatorSchwartz positionOperatorSchwartz Constants.ℏ	—	positionOperatorSchwartz_commutation_momentumOperatorSchwartz
positionOperatorSchwartz_commutation_momentumOperatorSchwartz 📖	mathematical	—	positionOperatorSchwartz momentumOperatorSchwartz Constants.ℏ	—	positionOperatorSchwartz_apply momentumOperatorSchwartz_apply positionOperatorSchwartz_apply_fun
positionOperatorSchwartz_momentumOperatorSchwartz_eq 📖	mathematical	—	positionOperatorSchwartz momentumOperatorSchwartz Constants.ℏ	—	positionOperatorSchwartz_commutation_momentumOperatorSchwartz

---

← Back to Index