instRingHomIdId

Mathlib.Algebra.Ring.CompTypeclasses

URI: https://scilib.ai/kg/mathlib#instRingHomIdId

English

The identity map on a ring R is a ring homomorphism that acts as the identity on every element.

Русский

Тождественный отображение на кольце R является кольцевым гомоморфизмом и действует как тождество на каждом элементе.

LaTeX

$$$\forall x \in R, \operatorname{id}_R(x) = x$$$

Lean4

instance {R : Type*} [Semiring R] : RingHomId (RingHom.id R) where eq_id := rfl

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

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

Разделы

Аффилиация

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