refl_toCoalgHom

Mathlib.RingTheory.Coalgebra.Equiv

URI: https://scilib.ai/kg/mathlib#CoalgEquiv.refl_toCoalgHom

English

The identity coalgebra equivalence corresponds to the identity coalgebra homomorphism.

Русский

Идентичная коалгебраическая эквивалентность соответствует идентичному коалгебраическому гомоморфизму.

LaTeX

$$$\\text{refl } R\\; A = \\text{CoalgHom.id } R\\; A$$$

Lean4

@[simp]
theorem refl_toCoalgHom : refl R A = CoalgHom.id R A :=
  rfl

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

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

Разделы

Аффилиация

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