Theorem LieAlgebra.SemiDirectSum.toProd_apply

Modification history

2026-08-28 12:39
Mathlib/Algebra/Lie/SemiDirect.lean
feat: semidirect product of Lie algebras - adding simp lemmas for toProd.symm and toProdl.symm (#41890) …
Modified LieAlgebra.SemiDirectSum.toProd_applyView on Github →
2026-03-22 21:51
Mathlib/Algebra/Lie/SemiDirect.lean
feat: compatible (pairs of) derivations form a Lie algebra (#36651) …
Added LieAlgebra.SemiDirectSum.toProd_applyView on Github →