inv_card_commutator_le_commProb — Mathlib

English

Same as Subgroup Bound: for any subgroup H ≤ G, mid-level bound for commProb(H) in terms of G and H.index.

Русский

То же самое, что и граница подгруппы: для любой подгруппы H ≤ G существует ограничение для commProb(H) через G и H.index.

LaTeX

$$commProb(H) \le commProb(G) \cdot (H.index)^2$$

Lean4

theorem inv_card_commutator_le_commProb : (↑(Nat.card (commutator G)))⁻¹ ≤ commProb G :=
  (inv_le_iff_one_le_mul₀ (Nat.cast_pos.mpr Finite.card_pos)).mpr
    (le_trans (ge_of_eq (commProb_eq_one_iff.mpr ⟨(Abelianization.commGroup G).mul_comm⟩))
      (commutator G).commProb_quotient_le)
      -- Construction of group with commuting probability 1/n

Похожие утверждения