Documentation Verification Report

CommutingProbability

📁 Source: Mathlib/GroupTheory/CommutingProbability.lean

Statistics

Metric	Count
Definitions `reciprocalFactors`, `commProb`	2
Theorems `commProb_cons`, `commProb_nil`, `commProb_odd`, `commProb_reciprocal`, `reciprocalFactors_even`, `reciprocalFactors_odd`, `reciprocalFactors_one`, `reciprocalFactors_zero`, `commProb_quotient_le`, `commProb_subgroup_le`, `commProb_def`, `commProb_def'`, `commProb_eq_one_iff`, `commProb_eq_zero_of_infinite`, `commProb_function`, `commProb_le_one`, `commProb_pi`, `commProb_pos`, `commProb_prod`, `inv_card_commutator_le_commProb`	20
Total	22

DihedralGroup

Definitions

Name	Category	Theorems
`reciprocalFactors` 📖	CompOp	5 math math: `reciprocalFactors_one`, `reciprocalFactors_zero`, `reciprocalFactors_odd`, `reciprocalFactors_even`, `commProb_reciprocal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commProb_cons` 📖	mathematical	—	`commProb` `Product` `Pi.instMul` `DihedralGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup`	—	`commProb_pi` `Finset.prod_congr` `Fin.prod_univ_succ`
`commProb_nil` 📖	mathematical	—	`commProb` `Product` `Pi.instMul` `DihedralGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup`	—	`commProb_pi` `Finset.prod_congr` `Finset.univ_eq_empty` `Fin.isEmpty'`
`commProb_odd` 📖	mathematical	`Odd` `Nat.instSemiring`	`commProb` `DihedralGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup`	—	`commProb_def'` `card_conjClasses_odd` `nat_card` `Nat.instAtLeastTwoHAddOfNat` `Nat.cast_div_charZero` `Rat.instCharZero` `Nat.odd_iff` `Nat.cast_add` `Nat.cast_mul` `div_div` `mul_assoc` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_ofNat`
`commProb_reciprocal` 📖	mathematical	—	`commProb` `Product` `reciprocalFactors` `Pi.instMul` `DihedralGroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup`	—	`reciprocalFactors_zero` `commProb_cons` `commProb_nil` `mul_one` `Nat.cast_zero` `div_zero` `commProb_eq_zero_of_infinite` `instInfiniteOfNatNat` `reciprocalFactors_one` `Nat.cast_one` `div_one` `Nat.even_or_odd` `reciprocalFactors_even` `commProb_odd` `Nat.instAtLeastTwoHAddOfNat` `Nat.cast_div` `Even.two_dvd` `Rat.instCharZero` `one_div` `inv_div` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `Nat.cast_pos'` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `NeZero.charZero_one` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_add` `reciprocalFactors_odd` `Odd.mul` `div_mul_div_comm` `div_eq_div_iff` `LT.lt.ne'` `Odd.pos` `Nat.instNontrivial` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`reciprocalFactors_even` 📖	mathematical	`Even`	`reciprocalFactors`	—	`reciprocalFactors.eq_1`
`reciprocalFactors_odd` 📖	mathematical	`Odd` `Nat.instSemiring`	`reciprocalFactors`	—	`reciprocalFactors.eq_1` `Nat.not_even_iff_odd`
`reciprocalFactors_one` 📖	mathematical	—	`reciprocalFactors`	—	`reciprocalFactors.eq_def`
`reciprocalFactors_zero` 📖	mathematical	—	`reciprocalFactors`	—	`reciprocalFactors.eq_def`

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commProb_quotient_le` 📖	mathematical	—	`commProb` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `Nat.card` `SetLike.instMembership` `instSetLike`	—	`commProb_def'` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Rat.instIsStrictOrderedRing` `Nat.cast_pos` `IsStrictOrderedRing.toIsOrderedRing` `Rat.nontrivial` `Finite.card_pos` `finite_quotient_of_finiteIndex` `finiteIndex_of_finite` `mul_assoc` `Nat.cast_mul` `index.eq_1` `card_mul_index` `div_mul_cancel₀` `Nat.cast_ne_zero` `Rat.instCharZero` `LT.lt.ne'` `One.instNonempty` `Nat.cast_le` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `Nat.card_le_card_of_surjective` `instFiniteConjClasses` `ConjClasses.map_surjective` `Quotient.mk''_surjective`
`commProb_subgroup_le` 📖	mathematical	—	`commProb` `Subgroup` `SetLike.instMembership` `instSetLike` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Monoid.toNatPow` `Rat.monoid` `index`	—	`commProb_def` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Rat.instIsStrictOrderedRing` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Rat.instZeroLEOneClass` `Nat.cast_pos` `IsStrictOrderedRing.toIsOrderedRing` `Rat.nontrivial` `Finite.card_pos` `instFiniteSubtypeMem` `One.instNonempty` `mul_assoc` `mul_pow` `Nat.cast_mul` `mul_comm` `card_mul_index` `div_mul_cancel₀` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `AddGroup.existsAddOfLE` `Nat.cast_ne_zero` `Rat.instCharZero` `LT.lt.ne'` `Nat.cast_le` `Rat.instAddLeftMono` `Nat.card_le_card_of_injective` `Subtype.finite` `Finite.instProd`

(root)

Definitions

Name	Category	Theorems
`commProb` 📖	CompOp	16 math math: `commProb_pos`, `DihedralGroup.commProb_nil`, `commProb_eq_zero_of_infinite`, `commProb_eq_one_iff`, `commProb_prod`, `commProb_pi`, `commProb_function`, `Subgroup.commProb_subgroup_le`, `commProb_le_one`, `DihedralGroup.commProb_odd`, `commProb_def'`, `Subgroup.commProb_quotient_le`, `commProb_def`, `inv_card_commutator_le_commProb`, `DihedralGroup.commProb_cons`, `DihedralGroup.commProb_reciprocal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commProb_def` 📖	mathematical	—	`commProb` `Nat.card` `Commute` `Monoid.toNatPow` `Rat.monoid`	—	—
`commProb_def'` 📖	mathematical	—	`commProb` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Nat.card` `ConjClasses`	—	`commProb.eq_1` `card_comm_eq_card_conjClasses_mul_card` `Nat.cast_mul` `sq` `MulZeroClass.zero_mul` `div_zero` `mul_div_mul_right`
`commProb_eq_one_iff` 📖	mathematical	—	`commProb`	—	`commProb.eq_1` `Set.coe_setOf` `Nat.card_eq_fintype_card` `div_eq_one_iff_eq` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Rat.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Nat.cast_ne_zero` `Rat.instCharZero` `Fintype.card_ne_zero` `Nat.cast_pow` `sq` `Fintype.card_prod` `set_fintype_card_eq_univ_iff` `Set.eq_univ_iff_forall`
`commProb_eq_zero_of_infinite` 📖	mathematical	—	`commProb`	—	`div_eq_zero_iff` `Nat.cast_eq_zero` `Rat.instCharZero` `Nat.card_eq_zero_of_infinite` `instInfiniteProdSubtypeCommute`
`commProb_function` 📖	mathematical	—	`commProb` `Pi.instMul` `Fintype.card`	—	`commProb_pi` `Finset.prod_const` `Finset.card_univ`
`commProb_le_one` 📖	mathematical	—	`commProb`	—	`div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Rat.instIsStrictOrderedRing` `Rat.instZeroLEOneClass` `Nat.cast_pow` `Nat.cast_le` `Rat.instAddLeftMono` `Rat.instCharZero` `sq` `Nat.card_prod` `Finite.card_subtype_le` `Finite.instProd` `sq_nonneg` `AddGroup.existsAddOfLE` `Rat.instPosMulMono`
`commProb_pi` 📖	mathematical	—	`commProb` `Pi.instMul` `Finset.prod` `Rat.commMonoid` `Finset.univ`	—	`Finset.prod_congr` `Finset.prod_div_distrib` `Finset.prod_pow` `Nat.card_congr`
`commProb_pos` 📖	mathematical	—	`commProb`	—	`div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Rat.instIsStrictOrderedRing` `Nat.cast_pos` `IsStrictOrderedRing.toIsOrderedRing` `Rat.nontrivial` `Finite.card_pos_iff` `Subtype.finite` `Finite.instProd` `pow_pos` `Rat.instZeroLEOneClass` `Finite.card_pos`
`commProb_prod` 📖	mathematical	—	`commProb` `Prod.instMul`	—	`div_mul_div_comm` `Nat.card_prod` `Nat.cast_mul` `mul_pow` `Nat.card_congr`
`inv_card_commutator_le_commProb` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `commutator` `commProb` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`inv_le_iff_one_le_mul₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Rat.instIsStrictOrderedRing` `Nat.cast_pos` `IsStrictOrderedRing.toIsOrderedRing` `Rat.nontrivial` `Finite.card_pos` `Subgroup.instFiniteSubtypeMem` `One.instNonempty` `le_trans` `ge_of_eq` `commProb_eq_one_iff` `instFiniteAbelianization` `CommGroup.mul_comm` `Subgroup.commProb_quotient_le`

---

← Back to Index