equiv_symm_eq_conj

Mathlib.GroupTheory.HNNExtension

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

English

For any b ∈ B, the image under φ.symm is conjugated by t^{-1} on the left of the image in B.

Русский

Для любого b ∈ B образ φ.symm переводится через сопряжение слева t^{-1} к образу b.

LaTeX

$$$ of(φ^{-1}(b)) = t^{-1} * of(b) * t \\quad (b \\in B) $$$

Lean4

theorem equiv_symm_eq_conj (b : B) : (of (φ.symm b : G) : HNNExtension G A B φ) = t⁻¹ * of (b : G) * t := by
  rw [mul_assoc, of_mul_t]; simp

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

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

Разделы

Аффилиация

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