toAut_inv

Mathlib.CategoryTheory.SingleObj

URI: https://scilib.ai/kg/mathlib#Units.toAut_inv

English

The inverse in Units M corresponds to the inverse endomorphism of the star object.

Русский

Обратный элемент в Units(M) соответствует обратному концевому морфизму звезды.

LaTeX

$$$\\text{toAut}\\,M\\,(x)^{-1} = \\text{toEnd}\\,M\\,(x^{-1})$$$

Lean4

@[simp]
theorem toAut_inv (x : Mˣ) : (toAut M x).inv = SingleObj.toEnd M (x⁻¹ : Mˣ) :=
  rfl

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

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

Разделы

Аффилиация

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