Commutation relations

The commutation relations between different operators.

Commutation relation betwen position and momentum operators

theorem QuantumMechanics.OneDimension.positionOperatorSchwartz_commutation_momentumOperatorSchwartz (ψ : SchwartzMap ℝ ℂ) : positionOperatorSchwartz (momentumOperatorSchwartz ψ) - momentumOperatorSchwartz (positionOperatorSchwartz ψ) = (Complex.I * ↑↑Constants.ℏ) • ψ

theorem QuantumMechanics.OneDimension.positionOperatorSchwartz_momentumOperatorSchwartz_eq (ψ : SchwartzMap ℝ ℂ) : positionOperatorSchwartz (momentumOperatorSchwartz ψ) = momentumOperatorSchwartz (positionOperatorSchwartz ψ) + (Complex.I * ↑↑Constants.ℏ) • ψ

theorem QuantumMechanics.OneDimension.momentumOperatorSchwartz_positionOperatorSchwartz_eq (ψ : SchwartzMap ℝ ℂ) : momentumOperatorSchwartz (positionOperatorSchwartz ψ) = positionOperatorSchwartz (momentumOperatorSchwartz ψ) - (Complex.I * ↑↑Constants.ℏ) • ψ