transferCenterPow_apply — Mathlib

English

The simple evaluation of transferCenterPow shows its underlying element is exactly the corresponding power.

Русский

Простое вычисление transferCenterPow даёт именно соответствующую степень.

LaTeX

$$$\uparrow(\mathrm{transferCenterPow}\;G\;g) = g^{(\mathrm{center}(G)).index}$$$

Lean4

@[simp]
theorem transferCenterPow_apply [FiniteIndex (center G)] (g : G) : ↑(transferCenterPow G g) = g ^ (center G).index :=
  rfl

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