instIsIsoInv

Mathlib.CategoryTheory.Monoidal.Grp_

URI: https://scilib.ai/kg/mathlib#GrpObj.instIsIsoInv

English

For any object A with a group structure, the unit morphism ι_A is an isomorphism.

Русский

Для любого объекта A с групповой структурой единичный морфизм ι_A является изоморфизмом.

LaTeX

$$$IsIso(\iota_A)$$$

Lean4

instance (A : C) [GrpObj A] : IsIso ι[A] :=
  ⟨ι, by simp, by simp⟩

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

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

Разделы

Аффилиация

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