instOneId

Mathlib.Algebra.Algebra.NonUnitalHom

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgHom.instOneId

English

There is a unit (or unit element) in the hom-set A →ₙₐ[R] A, given by the identity morphism on A.

Русский

Существует единичный элемент в множестве морфизмов A →ₙₐ[R] A, задаваемый тождественным гомоморфизмом на A.

LaTeX

$$$1_{A \to_{\mathrm{NonUnitalAlgHom}} A} = \mathrm{Id}_{R,A}$$$

Lean4

instance : One (A →ₙₐ[R] A) :=
  ⟨NonUnitalAlgHom.id R A⟩

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

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

Разделы

Аффилиация

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