coe_toMonoidHom

Mathlib.Algebra.Star.MonoidHom

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

English

If two StarMonoidHoms agree on every input, they are equal.

Русский

Если два отображения StarMonoidHom совпадают на всех входах, они равны.

LaTeX

$$∀ {f g : A →⋆* B}, (∀ x, f x = g x) → f = g$$

Lean4

@[simp]
theorem coe_toMonoidHom (f : A →⋆* B) : ⇑f.toMonoidHom = f :=
  rfl

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

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

Разделы

Аффилиация

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