Commit 2025-01-03 11:02 150f720a

feat(Algebra/Lie): add LieTower typeclass abstracting the Leibniz rule (#20403) This PR is a preparation for follow-up work on Lie's theorem. In the proof of Lie's theorem, there are a number of different ways to infer bracket actions, and not all of them allowed rewriting by the leibniz_lie lemma. So the proof would be massaging terms of Lie ideals into terms of the ambient Lie algebra, etc... By abstracting this lemma, and providing suitable instances, we can now simply rewrite with leibniz_lie without the massaging.