Commit 2026-07-28 15:41 4660688d
View on Github →feat: Transferring Lie Algebra structures along Equivalences (#39818)
This pr adds the functionality to transfer Lie brackets along equivalences (additive, linear and plain ones).
I followed the scheme of the existing TransferInstance.lean file.
For one of the proofs, I also needed linearEquiv_apply , which seemed missing so I added it.
AI use disclaimer: I used claude to search for lemmas/ understand error messages / proofreading and feedback, but wrote the whole code myself.