Commit 2026-08-28 12:39 41136d93

View on Github →

feat: semidirect product of Lie algebras - adding simp lemmas for toProd.symm and toProdl.symm (#41890) As an R-module the semidirect product of two Lie algebras K ⋊⁅ψ⁆ L is isomorphic to K × L. The simp lemmas for the reverse direction of this isomorphisms were missing and are added in this PR.

Estimated changes

Modified Mathlib/Algebra/Lie/SemiDirect.lean

modified theorem LieAlgebra.SemiDirectSum.toProd_apply

added theorem LieAlgebra.SemiDirectSum.toProd_symm_apply

added theorem LieAlgebra.SemiDirectSum.toProdl_symm_coe