toHopfAlgEquiv_refl

Mathlib.Algebra.Category.HopfAlgCat.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Iso.toHopfAlgEquiv_refl

English

The Hopf algebra equivalence associated to the identity isomorphism is the identity Hopf algebra equivalence.

Русский

Связанный с тождественным изоморфизмом эквивалент HopfAlg равен тождественному эквиваленту HopfAlg.

LaTeX

$$$toHopfAlgEquiv(\mathrm{refl}\, X) = \mathrm{refl}\ _\ _$$$

Lean4

@[simp]
theorem toHopfAlgEquiv_refl : toHopfAlgEquiv (.refl X) = .refl _ _ :=
  rfl

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

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

Разделы

Аффилиация

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