English
There is a canonical map from any F with AlgEquivClass to an actual AlgEquiv R A B; this provides a natural coercion to AlgEquiv.
Русский
Существует каноническое отображение из любого F, имеющего AlgEquivClass, в фактическое AlgEquiv R A B; обеспечивает естественное приведение к AlgEquiv.
LaTeX
$$$\\text{toAlgEquiv}: F \\to AlgEquiv(R,A,B)$$$
Lean4
/-- Turn an element of a type `F` satisfying `AlgEquivClass F R A B` into an actual `AlgEquiv`.
This is declared as the default coercion from `F` to `A ≃ₐ[R] B`. -/
@[coe]
def toAlgEquiv {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] (f : F) : A ≃ₐ[R] B :=
{ (f : A ≃ B), (f : A ≃+* B) with commutes' := commutes f }
