coe_toSubmodule — Mathlib

English

The embedding of a LieSubalgebra into Submodule respects the carrier subset, i.e., L' viewed as Submodule is the same as L' viewed as a set.

Русский

Вложение подалгебры в подподмножество сохраняет носитель: L' как Submodule соответствует L'.

LaTeX

$$$$\forall {R} {L} [\text{CommRing } R] [\text{LieRing } L] [\text{LieAlgebra } R L]\ (L' : \text{LieSubalgebra } R L),\ ((L' : Submodule R L) : Set L) = L'. $$$$

Lean4

theorem coe_toSubmodule : ((L' : Submodule R L) : Set L) = L' :=
  rfl

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