Skip to content

feat(QuantumMechanics): Add operator monoid#1132

Merged
jstoobysmith merged 5 commits into
leanprover-community:masterfrom
gloges:op-module
May 29, 2026
Merged

feat(QuantumMechanics): Add operator monoid#1132
jstoobysmith merged 5 commits into
leanprover-community:masterfrom
gloges:op-module

Conversation

@gloges
Copy link
Copy Markdown
Contributor

@gloges gloges commented May 28, 2026

Introduces an instance of Monoid for LinearPMap using the restricted composition defined in #1127. This allows one to take powers of operators, a prerequisite for defining the exponential map (e.g. for QHO coherent states).

Also adds a few basic lemmas about compRestricted and operator powers.

@gloges
Copy link
Copy Markdown
Contributor Author

gloges commented May 28, 2026

t-quantum-mechanics

@github-actions github-actions Bot added the t-quantum-mechanics Quantum mechanics label May 28, 2026
Copy link
Copy Markdown
Member

@jstoobysmith jstoobysmith left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good - approved. Will merge shortly.

@jstoobysmith jstoobysmith added the ready-to-merge This PR is approved and will be merged shortly label May 29, 2026
@jstoobysmith jstoobysmith merged commit 3855afe into leanprover-community:master May 29, 2026
4 checks passed
@gloges gloges deleted the op-module branch May 29, 2026 07:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR is approved and will be merged shortly t-quantum-mechanics Quantum mechanics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants