Theorems · Definition · group theory
Subgroup.QuotientDiff
{G : Type u_1} → [inst : Group G] → (H : Subgroup G) → [IsMulCommutative ↥H] → [H.FiniteIndex] → Type u_1The quotient of the transversals of an abelian normal N by the diff relation.
- Defined in
- Mathlib.GroupTheory.SchurZassenhaus
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- MonoidHom.idproof · cited by 323
- Subgroup.FiniteIndexstatement and proof · cited by 113
- IsMulCommutativestatement and proof · cited by 95
- Subgroup.LeftTransversalproof · cited by 13
- Subgroup.leftTransversals.diffproof · cited by 8
Cited by3
Results whose statement or proof uses this declaration.
- Subgroup.eq_one_of_smul_eq_onestatement and proof · cited by 1
- Subgroup.exists_smul_eqstatement and proof · cited by 1
- Subgroup.isComplement'_stabilizer_of_coprimestatement and proof · cited by 0