instCoeTCAlgEquiv — Mathlib

English

There exists a canonical coercion from F to AlgEquiv R A B (i.e., a CoeTC instance).

Русский

Существует каноническое приведение из F к AlgEquiv R A B (существует экземпляр CoeTC).

LaTeX

$$CoeTC F (AlgEquiv R A B)$$

Lean4

instance (F R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [EquivLike F A B]
    [AlgEquivClass F R A B] : CoeTC F (A ≃ₐ[R] B) :=
  ⟨toAlgEquiv⟩

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