jacobson_eq_bot

Mathlib.RingTheory.Jacobson.Ideal

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

English

If Jac(I) = ⊥, then I = ⊥.

Русский

Если Jac(I) = ⊥, то I = ⊥.

LaTeX

$$$\operatorname{jacobson}(I) = \bot \rightarrow I = \bot$$$

Lean4

theorem jacobson_eq_bot : jacobson I = ⊥ → I = ⊥ := fun h => eq_bot_iff.mpr (h ▸ le_jacobson)

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

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

Разделы

Аффилиация

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