id_right

Mathlib.Logic.Function.Conjugate

URI: https://scilib.ai/kg/mathlib#Function.Commute.id_right

English

Any self-map commutes with the identity map.

Русский

Любая самоперенос (отображение) коммутирует с тождественным отображением.

LaTeX

$$$ \text{Commute } f \ id $$$

Lean4

/-- Any self-map commutes with the identity map. -/
theorem id_right : Commute f id :=
  Semiconj.id_right

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

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

Разделы

Аффилиация

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