LaplaceRungeLenzVector

📁 Source: PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean

Statistics

Metric	Count
Definitions lrlOperator, lrlOperatorSqr	2
Theorems angularMomentumSqr_commutation_lrlSqr, angularMomentum_commutation_lrl, angularMomentum_commutation_lrlSqr, hamiltonianReg_commutation_lrl, lrlOperatorSqr_eq, lrlOperator_eq, lrlOperator_eq', lrlOperator_eq'', lrl_commutation_lrl	9
Total	11
⚠️ With sorry angularMomentum_commutation_lrl	1

QuantumMechanics.HydrogenAtom

Definitions

Name	Category	Theorems
lrlOperator 📖	CompOp	6 math math: angularMomentum_commutation_lrl, lrlOperator_eq'', hamiltonianReg_commutation_lrl, lrl_commutation_lrl, lrlOperator_eq', lrlOperator_eq
lrlOperatorSqr 📖	CompOp	3 math math: angularMomentum_commutation_lrlSqr, lrlOperatorSqr_eq, angularMomentumSqr_commutation_lrlSqr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
angularMomentumSqr_commutation_lrlSqr 📖	mathematical	—	Space d Space.instNormedAddCommGroup Space.instInnerProductSpaceReal QuantumMechanics.angularMomentumOperatorSqr lrlOperatorSqr	—	QuantumMechanics.leibniz_lie angularMomentum_commutation_lrlSqr
angularMomentum_commutation_lrl 📖 ⚠️	mathematical	—	Space d Space.instNormedAddCommGroup Space.instInnerProductSpaceReal QuantumMechanics.angularMomentumOperator lrlOperator Constants.ℏ KroneckerDelta.kroneckerDelta	—	—
angularMomentum_commutation_lrlSqr 📖	mathematical	—	Space d Space.instNormedAddCommGroup Space.instInnerProductSpaceReal QuantumMechanics.angularMomentumOperator lrlOperatorSqr	—	QuantumMechanics.lie_leibniz angularMomentum_commutation_lrl
hamiltonianReg_commutation_lrl 📖	mathematical	—	Space d Space.instNormedAddCommGroup Space.instInnerProductSpaceReal hamiltonianReg lrlOperator Constants.ℏ k QuantumMechanics.radiusRegPowOperator QuantumMechanics.positionOperator QuantumMechanics.angularMomentumOperator QuantumMechanics.momentumOperator	—	QuantumMechanics.radiusRegPowOperator_comp_eq QuantumMechanics.radiusRegPowOperator_apply QuantumMechanics.positionOperator_apply
lrlOperatorSqr_eq 📖	mathematical	—	lrlOperatorSqr Space d Space.instNormedAddCommGroup Space.instInnerProductSpaceReal m hamiltonianReg QuantumMechanics.angularMomentumOperatorSqr Constants.ℏ k QuantumMechanics.radiusRegPowOperator	—	lrlOperator_eq' lrlOperator_eq'' QuantumMechanics.momentumOperatorSqr.eq_1 QuantumMechanics.radiusRegPowOperator_apply
lrlOperator_eq 📖	mathematical	—	lrlOperator Space d Space.instNormedAddCommGroup Space.instInnerProductSpaceReal QuantumMechanics.positionOperator QuantumMechanics.momentumOperatorSqr QuantumMechanics.momentumOperator Constants.ℏ m k QuantumMechanics.radiusRegPowOperator	—	lrlOperator.eq_1 QuantumMechanics.momentum_comp_commute QuantumMechanics.momentum_comp_position_eq KroneckerDelta.eq_one_of_same KroneckerDelta.sum_smul QuantumMechanics.momentumOperatorSqr.eq_1
lrlOperator_eq' 📖	mathematical	—	lrlOperator Space d Space.instNormedAddCommGroup Space.instInnerProductSpaceReal QuantumMechanics.angularMomentumOperator QuantumMechanics.momentumOperator Constants.ℏ m k QuantumMechanics.radiusRegPowOperator QuantumMechanics.positionOperator	—	lrlOperator_eq QuantumMechanics.momentum_comp_commute
lrlOperator_eq'' 📖	mathematical	—	lrlOperator Space d Space.instNormedAddCommGroup Space.instInnerProductSpaceReal QuantumMechanics.momentumOperator QuantumMechanics.angularMomentumOperator Constants.ℏ m k QuantumMechanics.radiusRegPowOperator QuantumMechanics.positionOperator	—	lrlOperator_eq'
lrl_commutation_lrl 📖	mathematical	—	Space d Space.instNormedAddCommGroup Space.instInnerProductSpaceReal lrlOperator Constants.ℏ m hamiltonianReg QuantumMechanics.angularMomentumOperator	—	lrlOperator_eq QuantumMechanics.radiusRegPowOperator_apply

---

← Back to Index