Theorems · Definition · group theory
commProb
(M : Type u_1) → [Mul M] → ℚ
The commuting probability of a finite type with a multiplication operation.
- Defined in
- Mathlib.GroupTheory.CommutingProbability
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Mul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by16
Results whose statement or proof uses this declaration.
- commProb_pistatement · cited by 3
- commProb_def'statement · cited by 2
- Subgroup.commProb_quotient_lestatement and proof · cited by 1
- DihedralGroup.commProb_consstatement and proof · cited by 1
- DihedralGroup.commProb_nilstatement and proof · cited by 1
- DihedralGroup.commProb_oddstatement · cited by 1
- commProb_defstatement · cited by 1
- commProb_eq_one_iffstatement · cited by 1
- commProb_eq_zero_of_infinitestatement · cited by 1
- inv_card_commutator_le_commProbstatement · cited by 0
- Subgroup.commProb_subgroup_lestatement and proof · cited by 0
- commProb_functionstatement and proof · cited by 0