lieModule — Mathlib

English

There is a natural LieModule structure on I given by restricting the LieModule structure of L along I ↪ L.

Русский

Существует естественная структура LieModule на I, полученная ограничением структуры LieModule L по включению I ↪ L.

LaTeX

$$$ \text{LieModule}_R(I,M) \cong \text{restriction of } \text{LieModule}_R(L,M).$$$

Lean4

/-- Transfer the `LieModule` instance from the coercion `LieIdeal → LieSubalgebra`. -/
instance lieModule (I : LieIdeal R L) : LieModule R I M :=
  LieSubalgebra.lieModule (I : LieSubalgebra R L)

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