instFiniteSubtypeMemSubmoduleRootSpanOfFinite

English

If ι is finite, then P.rootSpan S is a finite S-submodule of M.

Русский

При конечности множества индексов ι, корневая область P.rootSpan S является конечным подмодулем над S.

LaTeX

$$$[Module\;S\;M] \;[Finite\;ι]\;:\;\text{Module.Finite }S\;\bigl(P.rootSpan\;S\bigr)$$

Lean4

instance [Module S M] [Finite ι] : Module.Finite S <| P.rootSpan S :=
  Finite.span_of_finite S <| finite_range _

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