English
There is a LieRingModule L on Linear maps M →ᴲ R defined by bracket x with f via [x,f](m) = − f([x,m]).
Русский
Существует структура LieRingModule на L для линейных отображений M →ᴲ R, заданная скобкой [x,f](m) = −f([x,m]).
LaTeX
$$$[x,f](m) = -f([x,m])$$$
Lean4
/-- We could avoid defining this by instead defining a `LieRingModule L R` instance with a zero
bracket and relying on `LinearMap.instLieRingModule`. We do not do this because in the case that
`L = R` we would have a non-defeq diamond via `Ring.instBracket`. -/
instance instLieRingModule : LieRingModule L (M →ₗ[R] R)
where
bracket := fun x f ↦
{ toFun := fun m ↦ -f ⁅x, m⁆
map_add' := by simp [-neg_add_rev, neg_add]
map_smul' := by simp }
add_lie := fun x y m ↦ by ext n; simp [-neg_add_rev, neg_add]
lie_add := fun x m n ↦ by ext p; simp [-neg_add_rev, neg_add]
leibniz_lie := fun x m n ↦ by ext p; simp
