Theorems · Definition · group theory

Subgroup.transferFunction

{G : Type u_1} → [inst : Group G] → (H : Subgroup G) → G → G ⧸ H → G

The transfer transversal as a function. Given a ⟨g⟩-orbit q₀, g • q₀, ..., g ^ (m - 1) • q₀ in G ⧸ H, an element g ^ k • q₀ is mapped to g ^ k • g₀ for a fixed choice of representative g₀ of q₀.

Defined in

Mathlib.GroupTheory.Transfer

Cited by

4 results in Mathlib

Foundations

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

Assumes

Group