refl

Mathlib.RingTheory.Coalgebra.Equiv

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

English

The identity map on A is a coalgebra equivalence.

Русский

Идентичный отображение на A является коалгебраической эквивалентностью.

LaTeX

$$$\\text{refl} \\; R\\; A : A \\simeq_{\\ell_c[R]} A$$$

Lean4

/-- The identity map is a coalgebra equivalence. -/
@[refl, simps!]
def refl : A ≃ₗc[R] A :=
  { CoalgHom.id R A, LinearEquiv.refl R A with }

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

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

Разделы

Аффилиация

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