mathlib

3478a2af - feat(probability/ident_distrib): identically distributed random variables (#14024)