Commit 2023-02-18 15:48 bafc9b07

View on Github →

feat: port GroupTheory.CommutingProbability (#2284)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/Abelianization.lean

Created Mathlib/GroupTheory/CommutingProbability.lean

added theorem Subgroup.commProb_quotient_le

added theorem Subgroup.commProb_subgroup_le

added theorem card_comm_eq_card_conjClasses_mul_card

added def commProb

added theorem commProb_def'

added theorem commProb_def

added theorem commProb_eq_one_iff

added theorem commProb_le_one

added theorem commProb_pos

added theorem inv_card_commutator_le_commProb