of_mul_t

Mathlib.GroupTheory.HNNExtension

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

English

The image of φ(a) under the embedding equals t · of(a) · t^{-1} for all a ∈ A.

Русский

Образ φ(a) под вложением равен t · of(a) · t^{-1} для всех a ∈ A.

LaTeX

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

Lean4

theorem of_mul_t (b : B) : (of (b : G) : HNNExtension G A B φ) * t = t * of (φ.symm b : G) := by rw [t_mul_of]; simp

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

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

Разделы

Аффилиация

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