instNonUnitalAlgEquivClass

Mathlib.Algebra.Star.StarAlgHom

URI: https://scilib.ai/kg/mathlib#StarAlgEquiv.instNonUnitalAlgEquivClass

English

Instance giving that a StarAlgEquiv defines a NonUnitalAlgEquivClass between A and B.

Русский

Экземпляр, подтверждающий, что StarAlgEquiv определяет NonUnitalAlgEquivClass между A и B.

LaTeX

$$$ \text{instNonUnitalAlgEquivClass } F R A B $$$

Lean4

instance : NonUnitalAlgEquivClass (A ≃⋆ₐ[R] B) R A B
    where
  map_mul f := f.map_mul'
  map_add f := f.map_add'
  map_smulₛₗ := map_smul'

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

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

Разделы

Аффилиация

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