English
If H ⫽ G, then commProb(G/H) ≤ commProb(G) · |H|.
Русский
Если H нормальная в G, то commProb(G/H) ≤ commProb(G) · |H|.
LaTeX
$$commProb(G/H) \le commProb(G) \cdot |H|$$
Lean4
theorem commProb_quotient_le [H.Normal] : commProb (G ⧸ H) ≤ commProb G * Nat.card H := by
/- After rewriting with `commProb_def'`, we reduce to showing that `G` has at least as many
conjugacy classes as `G ⧸ H`. -/
rw [commProb_def', commProb_def', div_le_iff₀, mul_assoc, ← Nat.cast_mul, ← Subgroup.index, H.card_mul_index,
div_mul_cancel₀, Nat.cast_le]
· apply Nat.card_le_card_of_surjective
show Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))
exact ConjClasses.map_surjective Quotient.mk''_surjective
· exact Nat.cast_ne_zero.mpr Finite.card_pos.ne'
· exact Nat.cast_pos.mpr Finite.card_pos
