Skip to content

feat: QM operator commutators#930

Open
gloges wants to merge 6 commits intolean-phys-community:masterfrom
gloges:commutators
Open

feat: QM operator commutators#930
gloges wants to merge 6 commits intolean-phys-community:masterfrom
gloges:commutators

Conversation

@gloges
Copy link
Contributor

@gloges gloges commented Feb 8, 2026

Continuing from #926:

  1. positionOperator made sorry-free
  2. deriv_smul is replaced by two related lemmas (deriv_const_smul is needed in momentum commutator proof)
  3. Proofs added for commutators

@zhikaip
Copy link
Collaborator

zhikaip commented Feb 8, 2026

Hi, just a heads up that things may break due to #929, especially a lot of changes around SchwartzMap. It will probably be merged tomorrow and you might have to modify accordingly after PhysLean is bumped to v4.27.0.

@gloges
Copy link
Contributor Author

gloges commented Feb 9, 2026

Thanks, no issues with the bump.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants