[Merged by Bors] - feat: when the indicator is independent from a random variable#39749

EtienneC30 wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

EtienneC30:indep_indEtienneC30/mathlib4:indep_indCopy head branch name to clipboard