of_mul_inv_t

Mathlib.GroupTheory.HNNExtension

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

English

The relation is symmetric: for a ∈ A, of(a) · t^{-1} = t^{-1} · of(φ(a)).

Русский

Отношение симметрично: для a ∈ A выполняется of(a) · t^{-1} = t^{-1} · of(φ(a)).

LaTeX

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

Lean4

theorem of_mul_inv_t (a : A) : (of (a : G) : HNNExtension G A B φ) * t⁻¹ = t⁻¹ * of (φ a : G) := by rw [equiv_eq_conj];
  simp [mul_assoc]

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

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

Разделы

Аффилиация

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