inclusion — Mathlib

English

The coercion to ambient module respects inclusion maps.

Русский

Приведение к базовому модулю сохраняет включение.

LaTeX

$$coe_inclusion (m : N) : (inclusion h m : M) = m$$

Lean4

/-- Given two nested Lie submodules `N ⊆ N'`,
the inclusion `N ↪ N'` is a morphism of Lie modules. -/
def inclusion : N →ₗ⁅R,L⁆ N'
    where
  __ := Submodule.inclusion (show N.toSubmodule ≤ N'.toSubmodule from h)
  map_lie' := rfl

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