instAbelianCondensedMod

Mathlib.Condensed.Module

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

English

The category CondensedMod R is Abelian.

Русский

Категория CondensedMod R абелиева.

LaTeX

$$$\text{Abelian}(\text{CondensedMod } R)$$$

Lean4

noncomputable instance : Abelian (CondensedMod.{u} R) :=
  sheafIsAbelian

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

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

Разделы

Аффилиация

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