Basic

📁 Source: PhysLean/QuantumMechanics/OneDimension/GeneralPotential/Basic.lean

Statistics

Metric	Count
Definitions GeneralPotential, V, m, schrodingerOperator, potentialOperator	5
Theorems hm, schrodingerOperator_linear, momentumOperator_linear, momentumOperator_sq_linear, potentialOperator_linear	5
Total	10

QuantumMechanics.OneDimension

Definitions

Name	Category	Theorems
GeneralPotential 📖	CompData	—
potentialOperator 📖	CompOp	1 math math: potentialOperator_linear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
momentumOperator_linear 📖	mathematical	—	momentumOperator	—	—
momentumOperator_sq_linear 📖	—	momentumOperator	—	—	momentumOperator_linear
potentialOperator_linear 📖	mathematical	—	potentialOperator	—	—

QuantumMechanics.OneDimension.GeneralPotential

Definitions

Name	Category	Theorems
V 📖	CompOp	—
m 📖	CompOp	1 math math: hm
schrodingerOperator 📖	CompOp	1 math math: schrodingerOperator_linear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hm 📖	mathematical	—	m	—	—
schrodingerOperator_linear 📖	mathematical	QuantumMechanics.OneDimension.momentumOperator	schrodingerOperator	—	QuantumMechanics.OneDimension.momentumOperator_sq_linear

---

← Back to Index