Theorems · Theorem · group theory

Subgroup.transferFunction_apply

∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (g : G) (q : G ⧸ H),
  H.transferFunction g q =
    g ^ ((H.quotientEquivSigmaZMod g) q).snd.cast * Quotient.out (Quotient.out ((H.quotientEquivSigmaZMod g) q).fst)

Defined in

Mathlib.GroupTheory.Transfer

Cited by

3 results in Mathlib

Foundations

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

Assumes

Group