toAlgEquiv — Mathlib

English

The algebra equivalence underlying a bialgebra equivalence induces an AlgEquivClass.

Русский

Алгебраическая эквивалентность, лежащая в основе биалгебровой эквивалентности, индуцирует AlgEquivClass.

LaTeX

$$$\\text{toAlgEquivClass}: F \\Rightarrow AlgEquivClass$$$

Lean4

/-- The algebra equivalence underlying a bialgebra equivalence. -/
def toAlgEquiv (f : A ≃ₐc[R] B) : A ≃ₐ[R] B :=
  { f.toCoalgEquiv with
    map_mul' := map_mul f.toMulEquiv
    map_add' := map_add f.toCoalgEquiv
    commutes' := AlgHomClass.commutes f.toBialgHom }

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