Structures · Algebra

IsLieTower

A tower of Lie bracket actions encapsulates the Leibniz rule for Lie bracket actions. More precisely, it does so in a relative setting: Let L₁ and L₂ be two types with Lie bracket actions on a type M endowed with an addition, and additionally assume a Lie bracket action of L₁ on L₂. Then the Leibniz rule asserts for all x : L₁, y : L₂, and m : M that ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ holds. Common examples include the case where L₁ is a Lie subalgebra of L₂ and the case where L₂ is a Lie ideal of L₁.

Defined in

Mathlib.Algebra.Lie.Basic

Shape

3 explicit arguments · adds leibniz_lie