instAlgHomClass — Mathlib

English

If F is a StarAlgEquiv between A and B with appropriate structure, then F has a NonUnitalAlgEquivClass instance.

Русский

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

LaTeX

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

Lean4

instance (priority := 100) instAlgHomClass (F R A B : Type*) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B]
    [Algebra R B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] : AlgEquivClass F R A B :=
  { commutes := fun f r => by simp only [Algebra.algebraMap_eq_smul_one, map_smul, map_one] }

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