instStarHomClass

Mathlib.Algebra.Star.MonoidHom

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

English

StarMonoidHom forms a StarHomClass: maps preserve star operation as well as multiplication.

Русский

StarMonoidHom образует StarHomClass: отображения сохраняют star и умножение.

LaTeX

$$StarMonoidHom A B ∈ StarHomClass A B$$

Lean4

instance : StarHomClass (A →⋆* B) A B where map_star f := f.map_star'

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

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

Разделы

Аффилиация

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