English
The largest L-invariant submodule of M on which L acts trivially is called the maximal trivial submodule, denoted maxTrivSubmodule R L M.
Русский
Наибольший подмодуль M, на котором L действует тривиально, называется максимальным тривиальным подмодулем, обозначаемым maxTrivSubmodule R L M.
LaTeX
$$$\\text{maxTrivSubmodule } R L M \\subseteq M$ is the largest submodule on which $L$ acts trivially.$$
Lean4
/-- The largest submodule of a Lie module `M` on which the Lie algebra `L` acts trivially. -/
def maxTrivSubmodule : LieSubmodule R L M
where
carrier := {m | ∀ x : L, ⁅x, m⁆ = 0}
zero_mem' x := lie_zero x
add_mem' {x y} hx hy z := by rw [lie_add, hx, hy, add_zero]
smul_mem' c x hx y := by rw [lie_smul, hx, smul_zero]
lie_mem {x m} hm y := by rw [hm, lie_zero]
