English
The coercion of transferCenterPow equals the same power, i.e., the center power map sends g to the power corresponding to the index of the center.
Русский
Коэрция transferCenterPow совпадает с той же степенью: отображение центра передаёт g в степень, соответствующую индексу центра.
LaTeX
$$$\uparrow(\mathrm{transferCenterPow}(G,g)) = g^{|\mathrm{center}(G)|}$$$
Lean4
/-- The transfer homomorphism `G →* center G`. -/
noncomputable def transferCenterPow [FiniteIndex (center G)] : G →* center G
where
toFun g := ⟨g ^ (center G).index, (center G).pow_index_mem g⟩
map_one' := Subtype.ext (one_pow (center G).index)
map_mul' a b := by simp_rw [← show ∀ _, (_ : center G) = _ from transfer_center_eq_pow, map_mul]
