instEquivLike — Mathlib

English

Equivalence-like structure on BialgEquiv is provided as an instance.

Русский

Класс эквивалентности задаёт структуру EquivLike на BialgEquiv.

LaTeX

$$$\\text{instance } : EquivLike (A \\simeq_{bialg} B) A B$$$

Lean4

instance : EquivLike (A ≃ₐc[R] B) A B where
  coe f := f.toFun
  inv := fun f => f.invFun
  coe_injective' _ _ h _ := toBialgHom_injective (DFunLike.coe_injective h)
  left_inv := fun f => f.left_inv
  right_inv := fun f => f.right_inv

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