instCoalgEquivClass — Mathlib

English

There is a CoalgEquivClass structure on A ≃ₗc[R] B, carrying map_add, map_smul, counit_comp, and map_comp_comul compatibilities with the coalgebra structures.

Русский

Существует структура CoalgEquivClass на A ≃ₗc[R] B, сохраняющая суммирование, скалярное умножение, согласование с кушителем, и совместимость с операциями коалгебры.

LaTeX

$$$\\text{CoalgEquivClass}(A \\simeq_{\\ell_c[R]} B)\\; R\\; A\\; B$$$

Lean4

instance : CoalgEquivClass (A ≃ₗc[R] B) R A B
    where
  map_add := (·.map_add')
  map_smulₛₗ := (·.map_smul')
  counit_comp := (·.counit_comp)
  map_comp_comul := (·.map_comp_comul)

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