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






leanprover-community/mathlib,leanprover-community/mathlib