instFinitePresentationForall

Mathlib.Algebra.Module.FinitePresentation

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

English

If ι is finite, then the module (ι →₀ R) has a finitely presented structure.

Русский

Если ι конечен, модуль (ι →₀ R) имеет конечнопредставимую структуру.

LaTeX

$$$[Finite ι] \Rightarrow Module.FinitePresentation R (ι \to₀ R)$$$

Lean4

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

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

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

Разделы

Аффилиация

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