Position

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

Statistics

Metric	Count
Definitions positionOperator, «term𝐱[_]»	2
Theorems positionOperator_apply, positionOperator_apply_fun	2
Total	4

QuantumMechanics

Definitions

Name	Category	Theorems
positionOperator 📖	CompOp	8 math math: angularMomentum_commutation_position, positionOperator_apply, angularMomentumOperator_apply_fun, position_commutation_momentum, position_commutation_position, angularMomentumSqr_commutation_position, positionOperator_apply_fun, angularMomentumOperator_apply
«term𝐱[_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
positionOperator_apply 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator Space.val	—	—
positionOperator_apply_fun 📖	mathematical	—	Space Space.instNormedAddCommGroup Space.instInnerProductSpaceReal positionOperator Space.val	—	—

---

← Back to Index