inv_t_mul_of

Mathlib.GroupTheory.HNNExtension

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

English

The inverse relation holds: t^{-1} · of(b) = of(φ.symm(b)) · t^{-1} for b ∈ B.

Русский

Справедливо обратное отношение: t^{-1} · of(b) = of(φ.symm(b)) · t^{-1} для b ∈ B.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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