coe_id

Mathlib.Algebra.Star.MonoidHom

URI: https://scilib.ai/kg/mathlib#StarMonoidHom.coe_id

English

The underlying map of the identity star-monoid homomorphism on A is the identity map on A.

Русский

Подлежащая карта тождественного звёздного моноидного гомоморфизма на A равна тождественному отображению на A.

LaTeX

$$$((\\mathrm{StarMonoidHom.id}\\ A) : A \\to A) = \\mathrm{id}_A$$$

Lean4

@[simp, norm_cast]
theorem coe_id : ⇑(StarMonoidHom.id A) = id :=
  rfl

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

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

Разделы

Аффилиация

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