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	11 math math: `angularMomentumOperator1D_trivial`, `angularMomentumOperatorSqr_apply_fun`, `angularMomentum_commutation_position`, `angularMomentumOperator_apply_fun`, `angularMomentum_commutation_angularMomentum`, `angularMomentumSqr_commutation_angularMomentum`, `angularMomentumOperatorSqr_apply`, `angularMomentumOperator_antisymm`, `angularMomentumOperator_eq_zero`, `angularMomentumOperator_apply`, `angularMomentum_commutation_momentum`
`angularMomentumOperator2D` 📖	CompOp	—
`angularMomentumOperator3D` 📖	CompOp	—
`angularMomentumOperatorSqr` 📖	CompOp	4 math math: `angularMomentumOperatorSqr_apply_fun`, `angularMomentumSqr_commutation_angularMomentum`, `angularMomentumOperatorSqr_apply`, `angularMomentumSqr_commutation_position`
`«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