instRingEmbeddingRing

Mathlib.CategoryTheory.Abelian.FreydMitchell

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.FreydMitchell.instRingEmbeddingRing

← MathLib Explorer

English

The object EmbeddingRing(C) carries a ring structure.

Русский

Объект EmbeddingRing(C) имеет структуру кольца.

LaTeX

$$$\operatorname{Ring}(\operatorname{EmbeddingRing}(C))$$$

Lean4

noncomputable instance : Ring (EmbeddingRing C) :=
  inferInstanceAs <|
    Ring <|
      IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing (Ind.yoneda (C := (AsSmall.{max u v} C)ᵒᵖ)).rightOp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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