eq_bot_of_comap_eq_bot

Mathlib.RingTheory.Ideal.GoingUp

URI: https://scilib.ai/kg/mathlib#Ideal.IsIntegralClosure.eq_bot_of_comap_eq_bot

← MathLib Explorer

English

Equivalently, if the comap is bottom then the ideal is bottom.

Русский

Соответственно, если образ обратного образа — ноль, то и сам идеал — ноль.

LaTeX

$$$$I^{\mathrm{comap}} = \bot \Rightarrow I = \bot.$$$$

Lean4

theorem eq_bot_of_comap_eq_bot [Nontrivial R] {I : Ideal A} : I.comap (algebraMap R A) = ⊥ → I = ⊥ :=
  by
  contrapose
  exact IsIntegralClosure.comap_ne_bot S

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

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

Разделы

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

Аффилиация

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