toSubgroupEquiv_one

Mathlib.GroupTheory.HNNExtension

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

English

Special case: the isomorphism at u = 1 is exactly φ.

Русский

Особый случай: изоморфизм при u = 1 совпадает с φ.

LaTeX

$$$toSubgroupEquiv(φ,1) = φ$$$

Lean4

@[simp]
theorem toSubgroupEquiv_one : toSubgroupEquiv φ 1 = φ :=
  rfl

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

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

Разделы

Аффилиация

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