conjMap_apply — Mathlib

English

Conjugation induces an equivariant map between stabilizers and their translates, compatible with h–g–k relations.

Русский

Конъугация индуцирует эквивариантное отображение между стабилизаторами и их трансляциями, совместимо с отношениями h, g, k.

LaTeX

$$$\mathrm{conjMap}: \mathrm{stabilizer\_EquivStabilizer} (hg) \to \mathrm{stabilizer\_EquivStabilizer} (hh)$$$

Lean4

@[to_additive]
theorem conjMap_apply (x : ofStabilizer G a) : (conjMap hg x : α) = g • x :=
  rfl

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