refl_toCoalgEquiv

Mathlib.RingTheory.Bialgebra.Equiv

URI: https://scilib.ai/kg/mathlib#BialgEquiv.refl_toCoalgEquiv

English

The refl bialgebra equivalence corresponds to CoalgEquiv.refl on the coalgebra side.

Русский

Эквивалентность refl биалгебры соответствует-CoalgEquiv.refl на стороне коалгебры.

LaTeX

$$$\\text{refl}_{\\mathrm{Bialg}}(R,A) = \\mathrm{CoalgEquiv.refl}(R,A)$$$

Lean4

@[simp]
theorem refl_toCoalgEquiv : refl R A = CoalgEquiv.refl R A :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru