SchwartzSubmodule

📁 Source: PhysLean/QuantumMechanics/OneDimension/HilbertSpace/SchwartzSubmodule.lean

Statistics

Metric	Count
Definitions schwartzIncl	1
Theorems schwartzIncl_coe_ae, schwartzIncl_injective, schwartzIncl_inner	3
Total	4

QuantumMechanics.OneDimension.HilbertSpace

Definitions

Name	Category	Theorems
schwartzIncl 📖	CompOp	8 math math: QuantumMechanics.OneDimension.positionStates_generalized_eigenvector_positionOperatorUnbounded, parityOperatorUnbounded_isSelfAdjoint, schwartzIncl_inner, schwartzIncl_injective, schwartzIncl_coe_ae, QuantumMechanics.OneDimension.momentumOperatorUnbounded_isSelfAdjoint, QuantumMechanics.OneDimension.planeWaveFunctional_generalized_eigenvector_momentumOperatorUnbounded, QuantumMechanics.OneDimension.positionOperatorUnbounded_isSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
schwartzIncl_coe_ae 📖	mathematical	—	QuantumMechanics.OneDimension.HilbertSpace schwartzIncl	—	—
schwartzIncl_injective 📖	mathematical	—	QuantumMechanics.OneDimension.HilbertSpace schwartzIncl	—	—
schwartzIncl_inner 📖	mathematical	—	QuantumMechanics.OneDimension.HilbertSpace schwartzIncl	—	schwartzIncl_coe_ae

---

← Back to Index