of_subsingleton

Mathlib.Algebra.Module.FinitePresentation

URI: https://scilib.ai/kg/mathlib#Module.FinitePresentation.of_subsingleton

English

If M is a subsingleton, then M is finitely presented over R.

Русский

Если M — подмножество с единственным элементом, то M конечнопредставим.

LaTeX

$$$[Subsingleton M] \Rightarrow Module.FinitePresentation R M$$$

Lean4

instance (priority := 900) of_subsingleton [Subsingleton M] : Module.FinitePresentation R M :=
  .of_equiv (default : (Fin 0 → R) ≃ₗ[R] M)

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

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

Разделы

Аффилиация

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