instFinitePresentationFinsupp

Mathlib.Algebra.Module.FinitePresentation

URI: https://scilib.ai/kg/mathlib#instFinitePresentationFinsupp

English

If ι is finite, then the Finsupp module (ι →₀ R) is finitely presented over R.

Русский

Для конечного индекса ι модуль Finsupp(ι →₀ R) конечнопредставим над R.

LaTeX

$$$\text{Module.FinitePresentation } R (\iota \to\₀ R)$$$

Lean4

instance : Module.FinitePresentation R (ι →₀ R) :=
  Module.finitePresentation_of_projective _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru