toSubmodule_mk — Mathlib

English

The Submodule underlying the LieSubmodule obtained from p with the additional structure h is exactly p.

Русский

Подмодуль, лежащий в основе образованного из p с дополнительной структурой h, равен p.

LaTeX

$$$ ((\{ p with lie_mem := h \} : LieSubmodule R L M) : Submodule R M) = p $$$

Lean4

theorem toSubmodule_mk (p : Submodule R M) (h) : (({ p with lie_mem := h } : LieSubmodule R L M) : Submodule R M) = p :=
  by cases p; rfl

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