jacobson_mono

Mathlib.RingTheory.Jacobson.Ideal

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

← MathLib Explorer

English

If I ≤ J, then Jac(I) ≤ Jac(J).

Русский

Если I ⊆ J, то Jac(I) ⊆ Jac(J).

LaTeX

$$$I \le J \Rightarrow \operatorname{jacobson}(I) \le \operatorname{jacobson}(J)$$$

Lean4

@[mono]
theorem jacobson_mono {I J : Ideal R} : I ≤ J → I.jacobson ≤ J.jacobson :=
  by
  intro h x hx
  rw [jacobson, mem_sInf] at hx ⊢
  exact fun K ⟨hK, hK_max⟩ => hx ⟨Trans.trans h hK, hK_max⟩

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

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

Разделы

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

Аффилиация

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