id_toRingHom

Mathlib.Algebra.Algebra.Hom

URI: https://scilib.ai/kg/mathlib#AlgHom.id_toRingHom

English

The underlying RingHom of the identity AlgHom is the identity RingHom.

Русский

У сущности identity AlgHom соответствующий RingHom является тем же RingHom, что и идентичность.

LaTeX

$$$\\text{id\\_toRingHom} : (AlgHom.id R A : A \\to+* A) = RingHom.id _$$$

Lean4

@[simp]
theorem id_toRingHom : (AlgHom.id R A : A →+* A) = RingHom.id _ :=
  rfl

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

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

Разделы

Аффилиация

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