map

Mathlib.RingTheory.TwoSidedIdeal.Operations

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.map

Lean4

/-- Pushout of a two-sided ideal. Defined as the span of the image of a two-sided ideal under a ring
homomorphism.
-/
def map (I : TwoSidedIdeal R) : TwoSidedIdeal S :=
  span (f '' I)

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

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

Разделы

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

Аффилиация

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