instStarHomClass

Mathlib.Algebra.Star.StarAlgHom

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

English

StarHomClass induces a StarHomClass instance for NonUnitalStarAlgHom.

Русский

StarHomClass порождает инстанс StarHomClass для NonUnitalStarAlgHom.

LaTeX

$$$\text{instance } [\text{StarHomClass } (A \to⋆ₙₐ[R] B) A B]$$$

Lean4

instance : StarHomClass (A →⋆ₙₐ[R] B) A B where map_star f := f.map_star'

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

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

Разделы

Аффилиация

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