instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId

English

There is a directed system of subobjects built from membership maps and linear maps between finitely generated submodules, compatible with the inclusion maps.

Русский

Существует направленная система подобъектов, построенная из отображений принадлежности и линейных отображений между конечнопредставимыми подмодулями, совместимая с инклюзиями.

LaTeX

$$$\\text{DirectedSystem}\\; (\\text{Subtype mem})\\; (\\text{linear maps})\\; \\text{compatibility with inclusions}$$$

Lean4

instance : DirectedSystem _ (fgSystem R M · · · ·)
    where
  map_self _ _ := rfl
  map_map _ _ _ _ _ _ := rfl

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