instAB4StarCondensedMod

Mathlib.Condensed.AB

URI: https://scilib.ai/kg/mathlib#Condensed.instAB4StarCondensedMod

English

For any ring R, CondensedMod(R) satisfies AB4*.

Русский

Для любого кольца R CondensedMod(R) удовлетворяет AB4*.

LaTeX

$$$\\mathrm{AB4^*}(\\mathrm{CondensedMod}\\,R)$$$

Lean4

instance : AB4Star (CondensedMod.{u} R) where ofShape J := hasExactLimitsOfShape (ModuleCat R) (Discrete J)

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

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

Разделы

Аффилиация

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