t_mul_of — Mathlib

English

For any a ∈ A, t · of(a) = of(φ(a)) · t; i.e., conjugating the image of a by t moves it to the image under φ.

Русский

Для любого a ∈ A выполняется t · of(a) = of(φ(a)) · t; то есть конъугация образа a буквой t переводит его в φ(a).

LaTeX

$$$ t * of(a) = of(φ(a)) * t \\quad (a \\in A) $$$

Lean4

theorem t_mul_of (a : A) : t * (of (a : G) : HNNExtension G A B φ) = of (φ a : G) * t :=
  (Con.eq _).2 <| ConGen.Rel.of _ _ <| ⟨a, by simp⟩

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