comap

Mathlib.RingTheory.TwoSidedIdeal.Operations

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

Lean4

/-- Preimage of a two-sided ideal, as a two-sided ideal. -/
def comap : TwoSidedIdeal S →o TwoSidedIdeal R
    where
  toFun I := ⟨I.ringCon.comap f⟩
  monotone' := by
    intro I J h
    rw [le_iff] at h
    intro x
    specialize @h (f x)
    simpa [mem_iff, RingCon.comap]

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

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

Разделы

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

Аффилиация

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