transfer_center_eq_pow — Mathlib

English

In a group G with finite index of its center, the transfer from the center to itself sends g to the power g^{index}, i.e., transferCenterPow(g) = g^{index} in the center.

Русский

Для центра G, если индекс центра конечен, передача элементов центра в центр отправляет g в степень g^{index}.

LaTeX

$$$\mathrm{transferCenterPow}(G,g) = g^{|\,\mathrm{center}(G)\,|}$ in the center$$

Lean4

theorem transfer_center_eq_pow [FiniteIndex (center G)] (g : G) :
    transfer (MonoidHom.id (center G)) g = ⟨g ^ (center G).index, (center G).pow_index_mem g⟩ :=
  transfer_eq_pow (id (center G)) g fun k _ hk => by rw [← mul_right_inj, ← hk.comm, mul_inv_cancel_right]

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