instFinitePresentation

Mathlib.Algebra.Module.FinitePresentation

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

English

Instance asserting that the ring R is finitely presented as a module over itself.

Русский

Инстанс: кольцо R является конечнопредставимым как модуль над собой же.

LaTeX

$$$\text{Module.FinitePresentation } R R$$$

Lean4

instance : Module.FinitePresentation R R :=
  Module.finitePresentation_of_projective _ _

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

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

Разделы

Аффилиация

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