Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `HydrogenAtom`, `d`, `hamiltonianReg`, `k`, `m`	5
Theorems `hm`, `m_ne_zero`	2
Total	7

QuantumMechanics

Definitions

Name	Category	Theorems
`HydrogenAtom` 📖	CompData	—

QuantumMechanics.HydrogenAtom

Definitions

Name	Category	Theorems
`d` 📖	CompOp	9 math math: `angularMomentum_commutation_lrl`, `lrlOperator_eq''`, `hamiltonianReg_commutation_lrl`, `lrl_commutation_lrl`, `angularMomentum_commutation_lrlSqr`, `lrlOperator_eq'`, `lrlOperatorSqr_eq`, `lrlOperator_eq`, `angularMomentumSqr_commutation_lrlSqr`
`hamiltonianReg` 📖	CompOp	3 math math: `hamiltonianReg_commutation_lrl`, `lrl_commutation_lrl`, `lrlOperatorSqr_eq`
`k` 📖	CompOp	5 math math: `lrlOperator_eq''`, `hamiltonianReg_commutation_lrl`, `lrlOperator_eq'`, `lrlOperatorSqr_eq`, `lrlOperator_eq`
`m` 📖	CompOp	6 math math: `lrlOperator_eq''`, `lrl_commutation_lrl`, `lrlOperator_eq'`, `lrlOperatorSqr_eq`, `lrlOperator_eq`, `hm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hm` 📖	mathematical	—	`m`	—	—
`m_ne_zero` 📖	—	—	—	—	`hm`

---

← Back to Index