instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass

English

If F is a StarAlgEquiv between A and B with appropriate structure, then F belongs to the class NonUnitalAlgEquivClass, i.e., it respects addition, multiplication, and scalar action.

Русский

Если F является StarAlgEquiv между A и B с необходимой структурой, то F принадлежит классу NonUnitalAlgEquivClass, то есть он сохраняет сложение, умножение и скалярное действие.

LaTeX

$$$ \text{StarAlgEquivClass} \; F \; R \; A \; B \; \Rightarrow \text{NonUnitalAlgHomClass } F R A B $$$

Lean4

instance (priority := 100) {F R A B : Type*} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
    [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] :
    NonUnitalAlgHomClass F R A B :=
  { }
    -- See note [lower instance priority]

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