map_eq_id

Mathlib.Algebra.Algebra.Defs

URI: https://scilib.ai/kg/mathlib#Algebra.id.map_eq_id

English

The canonical algebra homomorphism from R to R is the identity map on R: algebraMap R R = id_R.

Русский

Канонический алгебраический гомоморфизм R → R совпадает с тождественным отображением.

LaTeX

$$$\\mathrm{algebraMap}\\, R\\, R = \\mathrm{id}_R$$$

Lean4

@[deprecated algebraMap_self (since := "2025-07-17")]
theorem map_eq_id : algebraMap R R = RingHom.id _ :=
  rfl

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

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

Разделы

Аффилиация

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