Documentation Verification Report

AngularMomentum

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

Statistics

Metric	Count
Definitions `angularMomentumOperator`, `angularMomentumOperator2D`, `angularMomentumOperator3D`, `angularMomentumOperatorSqr`, `«term𝐋[_,_]»`, `«term𝐋²»`	6
Theorems `angularMomentumOperator1D_trivial`, `angularMomentumOperatorSqr_apply`, `angularMomentumOperatorSqr_apply_fun`, `angularMomentumOperator_antisymm`, `angularMomentumOperator_apply`, `angularMomentumOperator_apply_fun`, `angularMomentumOperator_eq_zero`	7
Total	13

QuantumMechanics

Definitions

Name	Category	Theorems
`angularMomentumOperator` 📖	CompOp	21 math math: `HydrogenAtom.angularMomentum_commutation_lrl`, `angularMomentum_commutation_radiusRegPow`, `angularMomentumOperator1D_trivial`, `angularMomentumOperatorSqr_apply_fun`, `momentum_comp_angularMomentum_eq`, `angularMomentum_commutation_position`, `angularMomentumOperator_apply_fun`, `angularMomentum_commutation_angularMomentum`, `HydrogenAtom.lrlOperator_eq''`, `angularMomentumSqr_commutation_angularMomentum`, `angularMomentumOperatorSqr_apply`, `HydrogenAtom.hamiltonianReg_commutation_lrl`, `HydrogenAtom.lrl_commutation_lrl`, `HydrogenAtom.angularMomentum_commutation_lrlSqr`, `HydrogenAtom.lrlOperator_eq'`, `angularMomentumOperator_antisymm`, `angularMomentumOperator_eq_zero`, `momentumSqr_comp_angularMomentum_commute`, `angularMomentumOperator_apply`, `angularMomentum_commutation_momentumSqr`, `angularMomentum_commutation_momentum`
`angularMomentumOperator2D` 📖	CompOp	—
`angularMomentumOperator3D` 📖	CompOp	—
`angularMomentumOperatorSqr` 📖	CompOp	7 math math: `angularMomentumOperatorSqr_apply_fun`, `angularMomentumSqr_commutation_radiusRegPow`, `angularMomentumSqr_commutation_angularMomentum`, `angularMomentumOperatorSqr_apply`, `HydrogenAtom.lrlOperatorSqr_eq`, `angularMomentumSqr_commutation_momentumSqr`, `HydrogenAtom.angularMomentumSqr_commutation_lrlSqr`
`«term𝐋[_,_]»` 📖	CompOp	—
`«term𝐋²»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`angularMomentumOperator1D_trivial` 📖	mathematical	—	`angularMomentumOperator` `Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal`	—	`angularMomentumOperator_eq_zero`
`angularMomentumOperatorSqr_apply` 📖	mathematical	—	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `angularMomentumOperatorSqr` `angularMomentumOperator`	—	`angularMomentumOperatorSqr_apply_fun`
`angularMomentumOperatorSqr_apply_fun` 📖	mathematical	—	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `angularMomentumOperatorSqr` `angularMomentumOperator`	—	—
`angularMomentumOperator_antisymm` 📖	mathematical	—	`angularMomentumOperator` `Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal`	—	—
`angularMomentumOperator_apply` 📖	mathematical	—	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `angularMomentumOperator` `positionOperator` `momentumOperator`	—	—
`angularMomentumOperator_apply_fun` 📖	mathematical	—	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `angularMomentumOperator` `positionOperator` `momentumOperator`	—	—
`angularMomentumOperator_eq_zero` 📖	mathematical	—	`angularMomentumOperator` `Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal`	—	—

---

← Back to Index