Theorems · Theorem · group theory

MonoidHom.transferSylow_restrict_eq_pow

Deprecated since 2026-07-19Use MonoidHom.transferSylow_domRestrict_eq_pow instead.

∀ {G : Type u_1} [inst : Group G] {p : ℕ} (P : Sylow p G) (hP : Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P)
  [Fact (Nat.Prime p)] [Finite (Sylow p G)] [inst_3 : (↑P).FiniteIndex],
  ⇑((MonoidHom.transferSylow P hP).domRestrict ↑P) = fun x => x ^ (↑P).index

Alias of MonoidHom.transferSylow_domRestrict_eq_pow.

Defined in

Mathlib.GroupTheory.Transfer

Cited by

0 results in Mathlib

Foundations

Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupFactFiniteSubgroup.FiniteIndex