comap_ne_top

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#Ideal.comap_ne_top

← MathLib Explorer

English

If K is not the top ideal, then comap f K is not the top ideal.

Русский

Если K ≠ ⊤, то comap f K ≠ ⊤.

LaTeX

$$$ K \neq \top \Rightarrow \operatorname{comap} f K \neq \top $$$

Lean4

theorem comap_ne_top [RingHomClass F R S] (hK : K ≠ ⊤) : comap f K ≠ ⊤ :=
  (ne_top_iff_one _).2 <| by rw [mem_comap, map_one]; exact (ne_top_iff_one _).1 hK

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

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

Разделы

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

Аффилиация

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