Commutation

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

Statistics

Metric	Count
Definitions	0
Theorems angularMomentumSqr_commutation_angularMomentum, angularMomentumSqr_commutation_position, angularMomentum_commutation_angularMomentum, angularMomentum_commutation_momentum, angularMomentum_commutation_position, momentumSqr_commutation_momentum, momentum_commutation_momentum, momentum_momentum_eq, position_commutation_momentum, position_commutation_position	10
Total	10
⚠️ With sorry angularMomentumSqr_commutation_angularMomentum, angularMomentumSqr_commutation_position, angularMomentum_commutation_angularMomentum, angularMomentum_commutation_momentum, angularMomentum_commutation_position, momentum_commutation_momentum, position_commutation_momentum	7

QuantumMechanics

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angularMomentumSqr_commutation_angularMomentum 📖 ⚠️	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperatorSqr angularMomentumOperator	—	—
angularMomentumSqr_commutation_position 📖 ⚠️	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperatorSqr positionOperator	—	—
angularMomentum_commutation_angularMomentum 📖 ⚠️	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperator Constants.ℏ	—	—
angularMomentum_commutation_momentum 📖 ⚠️	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperator momentumOperator Constants.ℏ	—	—
angularMomentum_commutation_position 📖 ⚠️	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal angularMomentumOperator positionOperator Constants.ℏ	—	—
momentumSqr_commutation_momentum 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperatorSqr momentumOperator	—	momentum_momentum_eq
momentum_commutation_momentum 📖 ⚠️	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperator	—	—
momentum_momentum_eq 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal momentumOperator	—	momentum_commutation_momentum
position_commutation_momentum 📖 ⚠️	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator momentumOperator Constants.ℏ	—	—
position_commutation_position 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator	—	—

---

← Back to Index