jacobson_quotient_jacobson

Mathlib.RingTheory.Jacobson.Radical

URI: https://scilib.ai/kg/mathlib#Module.jacobson_quotient_jacobson

English

If f is injective and jacobson of the target is ⊥, then jacobson of the source is ⊥.

Русский

Если f инъективно отображает и jacobson целевого равен 0, то jacobson исходного равен 0.

LaTeX

$$jacobson R M = ⊥$$

Lean4

@[simp]
theorem jacobson_quotient_jacobson : jacobson R (M ⧸ jacobson R M) = ⊥ := by
  rw [jacobson_quotient_of_le le_rfl, mkQ_map_self]

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

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

Разделы

Аффилиация

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