toAlgEquivClass — Mathlib

English

For a bialgebra equivalence f, there is a corresponding algebra equivalence underlying it.

Русский

Для биалгебровой эквивалентности f существует соответствующая алгебраическая эквивалентность, лежащая в ее основе.

LaTeX

$$$f \\text{ yields } f_{Alg} : A \\to_{Alg} B$$$

Lean4

instance (priority := 100) toAlgEquivClass : AlgEquivClass F R A B
    where
  map_mul := map_mul
  map_add := map_add
  commutes := AlgHomClass.commutes

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