feat(QuantumMechanics): Add TODOs

[gloges]

Adds a number of quantum mechanics TODOs.
Some are currently possible to complete (e.g. the operator examples), but others depend on areas such as (degenerate) perturbation theory which are currently undeveloped and can help guide further development.

Q: Is there a better way to refer to other TODOs? In one of the momentum TODOs I have used the hash of the other.

[gloges]

t-quantum-mechanics

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[jstoobysmith]

Nice! Looks good. APproved.

[jstoobysmith]

Is there a better way to refer to other TODOs? In one of the momentum TODOs I have used the hash of the other.

The hash is probably the unique way to identify them, although we should probably make a tool which allows people to find TODOs by their hashes.

[gloges]

Thanks! Perhaps TODOs could have an (optional) second ID in addition to the hash which is user-picked and human readable, but not necessarily unique. e.g. something like "QM-momentum-domain" for the one I mentioned. The non-uniqueness may even be a pro since it allows related TODOs to be found simultaneously in a search.

[jstoobysmith]

Yeah agreed! For now you could probably preface your TODO string with "QM-momentum-domain: ....", and use that instead. Won't merge just yet in case you want to do this.

[gloges]

I think it's okay for now - merge away!