t_pow_smul_eq_unitsSMul — Mathlib

English

There is a natural equivalence between the HNN extension and words in normal form, given by mapping an element to its word and extracting a word to the element.

Русский

Существует естественное эквивалентное соответствие между HNN-расширением и словами в нормальной форме: элемент ↔ слово, слово ↔ элемент.

LaTeX

$$$\\mathrm{equiv} : \\mathrm{HNNExtension}\\; G\\; A\\; B\\; \\varphi \\;\\simeq\\; \\mathrm{NormalWord}\\; d.$$$

Lean4

theorem t_pow_smul_eq_unitsSMul (u : ℤˣ) (w : NormalWord d) :
    (t ^ (u : ℤ) : HNNExtension G A B φ) • w = unitsSMul φ u w := by
  rcases Int.units_eq_one_or u with (rfl | rfl) <;> simp [instHSMul, SMul.smul, MulAction.toEndHom, Equiv.Perm.inv_def]

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