comap_jacobson_of_ker_le

Mathlib.RingTheory.Jacobson.Radical

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

← MathLib Explorer

English

If f is bijective, comap f (jacobson R₂ M₂) equals 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_ker_le (surj : Function.Surjective f) (le : LinearMap.ker f ≤ jacobson R M) :
    comap f (jacobson R₂ M₂) = jacobson R M := by rw [← map_jacobson_of_ker_le surj le, comap_map_eq_self le]

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

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

Разделы

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

Аффилиация

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