toSubgroupEquiv_neg_one

Mathlib.GroupTheory.HNNExtension

URI: https://scilib.ai/kg/mathlib#HNNExtension.toSubgroupEquiv_neg_one

English

The isomorphism at u = -1 is the inverse φ^{-1}.

Русский

Изоморфизм при u = -1 равен φ^{-1}.

LaTeX

$$$toSubgroupEquiv(φ,-1) = φ^{-1}$$$

Lean4

@[simp]
theorem toSubgroupEquiv_neg_one : toSubgroupEquiv φ (-1) = φ.symm :=
  rfl

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

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

Разделы

Аффилиация

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