transferSylow_restrict_eq_pow — Mathlib

English

The transfer Sylow homomorphism, when restricted to P, is exactly the map x ↦ x^{[G:P]} on P.

Русский

Перенос Sylow, ограниченный до P, является именно отображением x ↦ x^{[G:P]} на P.

LaTeX

$$$\left(\operatorname{transferSylow}(P,h_P)\right)\restriction (P) = (\lambda x : P, x \mapsto x^{(P:G).index})$$$

Lean4

theorem transferSylow_restrict_eq_pow :
    ⇑((transferSylow P hP).restrict (P : Subgroup G)) = (fun x : P => x ^ (P : Subgroup G).index) :=
  funext fun g => transferSylow_eq_pow P hP g g.2

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