instCoeToBialgEquiv — Mathlib

English

Reinterpret an element of a type F of bialgebra equivalences as a BialgEquiv R A B.

Русский

Переинтерпретируем элемент типа F эквивалентностей биалгебр как биалгебровую эквивалентность.

LaTeX

$$$f : F \\Rightarrow BialgEquiv(R,A,B)$$$

Lean4

/-- Reinterpret an element of a type of bialgebra equivalences as a bialgebra equivalence. -/
instance instCoeToBialgEquiv : CoeHead F (A ≃ₐc[R] B) where coe f := toBialgEquiv f

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