instMonoidHomClass

Mathlib.Algebra.Star.MonoidHom

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

English

The type A →⋆* B forms a MonoidHomClass: maps preserve multiplication and identity.

Русский

Тип A →⋆* B образует MonoidHomClass: отображения сохраняют умножение и единицу.

LaTeX

$$StarMonoidHom A B ∈ MonoidHomClass A B$$

Lean4

instance : MonoidHomClass (A →⋆* B) A B where
  map_mul f := f.map_mul'
  map_one f := f.map_one'

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

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

Разделы

Аффилиация

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