`BookProof.ChapterAttentionCollision.inv_card_le_collisionProb` {p : Fin m → ℝ} (hsum : ∑ j, p j = 1) : (m : ℝ)⁻¹ ≤ collisionProb p

Initializing...

`BookProof.ChapterAttentionCollision.inv_card_le_collisionProb` {p : Fin m → ℝ} (hsum : ∑ j, p j = 1) : (m : ℝ)⁻¹ ≤ collisionProb p · Prove2Me