conj_eq_conj

Mathlib.Algebra.Category.ModuleCat.Basic

URI: https://scilib.ai/kg/mathlib#ModuleCat.Iso.conj_eq_conj

English

The endomorphism ring End M is isomorphic to the ring of linear endomorphisms of M.

Русский

Кольцо эндоморфизмов End M изоморфно кольцу линейных эндоморфизмов End_R(M).

LaTeX

$$End M ≃+* End_R(M)$$

Lean4

theorem conj_eq_conj (i : X ≅ X') (f : End X) : Iso.conj i f = ⟨LinearEquiv.conj i.toLinearEquiv f.hom⟩ :=
  rfl

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

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

Разделы

Аффилиация

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