commute_id_right

Mathlib.Algebra.Module.LinearMap.End

URI: https://scilib.ai/kg/mathlib#Module.End.commute_id_right

English

The identity map on an R-module M commutes with any endomorphism f: End_R(M): id ∘ f = f ∘ id.

Русский

Тождественный отображение на R-модуле M коммутирует с любым эндоморфизмом f: End_R(M): id ∘ f = f ∘ id.

LaTeX

$$Commute$LinearMap.id, f$$$

Lean4

theorem commute_id_right : Commute f LinearMap.id := by ext; simp

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

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

Разделы

Аффилиация

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