map_jacobson_of_bijective

Mathlib.RingTheory.Jacobson.Radical

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

← MathLib Explorer

English

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

Русский

Если f биективно, отображение jacobson(R,M) равняется jacobson(R₂,M₂).

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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