refl

Mathlib.RingTheory.Bialgebra.Equiv

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

English

The identity map on A is a bialgebra equivalence A ≃ₐc[R] A.

Русский

Идентити-отображение на A является биалгебровым эквивалентством A ≃ₐc[R] A.

LaTeX

$$$\\mathrm{id}_A : A \\to A \\text{ is a } A \\equiv_{\\mathrm{bialg}} A$$$

Lean4

/-- The identity map is a bialgebra equivalence. -/
@[refl, simps!]
def refl : A ≃ₐc[R] A :=
  { CoalgEquiv.refl R A, BialgHom.id R A with }

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

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

Разделы

Аффилиация

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