pow_zero

Mathlib.CategoryTheory.Equivalence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Equivalence.pow_zero

English

Any auto-equivalence raised to the 0th power is the identity equivalence.

Русский

Любая автэквивалентность в степени 0 равна идентичности.

LaTeX

$$$e^{0} = \mathrm{refl}$$$

Lean4

@[simp]
theorem pow_zero (e : C ≌ C) : e ^ (0 : ℤ) = Equivalence.refl :=
  rfl

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

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

Разделы

Аффилиация

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