jacobson_le_of_eq_bot

Mathlib.RingTheory.Jacobson.Radical

URI: https://scilib.ai/kg/mathlib#Ring.jacobson_le_of_eq_bot

← MathLib Explorer

English

If jacobson(R/I) = ⊥, then jacobson(R) ≤ I.

Русский

Если jacobson(R/I) = ⊥, то jacobson(R) ⊆ I.

LaTeX

$$$\\operatorname{jacobson}(R/I) = \\bot \\Rightarrow \\operatorname{jacobson}(R) \\le I.$$$

Lean4

theorem jacobson_le_of_eq_bot {I : Ideal R} [I.IsTwoSided] (h : jacobson (R ⧸ I) = ⊥) : jacobson R ≤ I :=
  Module.jacobson_le_of_eq_bot <| by
    rw [← le_bot_iff, ← SetLike.coe_subset_coe] at h ⊢
    rwa [← coe_jacobson_quotient]

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

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

Разделы

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

Аффилиация

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