idealComapOrderIso_symm_apply

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#RingEquiv.idealComapOrderIso_symm_apply

← MathLib Explorer

English

The inverse of the ideal correspondence applied to I equals I.map e.

Русский

Обратное отображение соответствия идеалов даёт I.map e.

LaTeX

$$$$ e.idealComapOrderIso.symm I = I.map e. $$$$

Lean4

@[simp]
theorem idealComapOrderIso_symm_apply {R S : Type*} [Semiring R] [Semiring S] (e : R ≃+* S) (I : Ideal R) :
    e.idealComapOrderIso.symm I = I.map e :=
  rfl

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

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

Разделы

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

Аффилиация

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