Theorems · Definition · group theory
Subgroup.transferTransversal
{G : Type u_1} → [inst : Group G] → (H : Subgroup G) → G → H.LeftTransversalThe transfer transversal. Contains elements of the form g ^ k • g₀ for fixed choices
of representatives g₀ of fixed choices of representatives q₀ of ⟨g⟩-orbits in G ⧸ H.
- Defined in
- Mathlib.GroupTheory.Transfer
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- Subgroupstatement and proof · cited by 3,593
- Subgroup.LeftTransversalstatement · cited by 13
- Subgroup.transferSetproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- Subgroup.transferTransversal_applystatement · cited by 2
- MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quotproof · cited by 2
- Subgroup.transferTransversal_apply'statement · cited by 1
- Subgroup.transferTransversal_apply''statement and proof · cited by 1