comap_jacobson_of_bijective

Mathlib.RingTheory.Jacobson.Radical

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

← MathLib Explorer

English

If f is bijective, comap f (jacobson R₂ M₂) = jacobson R M.

Русский

Если f биективно, то comap f (jacobson R₂ M₂) = jacobson R M.

LaTeX

$$comap f (jacobson R₂ M₂) = jacobson R M$$

Lean4

theorem comap_jacobson_of_bijective (hf : Function.Bijective f) : comap f (jacobson R₂ M₂) = jacobson R M :=
  comap_jacobson_of_ker_le hf.2 <| by simp_rw [(LinearMapClass.ker_eq_bot _).mpr hf.1, bot_le]

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

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

Разделы

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

Аффилиация

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