instIsTrivialSubtypeMemLieSubmoduleMaxTrivSubmodule

English

An L-module M is trivial if and only if the maximal trivial submodule equals the whole module M.

Русский

Модуль Ли M тривиален тогда и только тогда, когда максимальный тривиальный подмодуль равен всего модулю M.

LaTeX

$$$IsTrivial(L,M) \\iff maxTrivSubmodule R L M = \\top$$$

Lean4

instance : IsTrivial L (maxTrivSubmodule R L M) where trivial x m := Subtype.ext (m.property x)

Похожие утверждения