normalizer_bot_eq_maxTrivSubmodule

English

The normalizer of the bottom submodule coincides with the maximal triv submodule: (⊥).normalizer = LieModule.maxTrivSubmodule R L M.

Русский

Нормализатор нуля совпадает с максимальным тривиальным подмодулем: (⊥).normalizer = LieModule.maxTrivSubmodule R L M.

LaTeX

$$$ (\\perp : LieSubmodule R L M).normalizer = \\mathrm{LieModule.maxTrivSubmodule} \\ R\\ L\\ M $$$

Lean4

theorem normalizer_bot_eq_maxTrivSubmodule : (⊥ : LieSubmodule R L M).normalizer = LieModule.maxTrivSubmodule R L M :=
  rfl

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