Commit 2023-12-20 15:54 56c6c095

feat: f i * f j, f k * f l are independent if f is (#8971) Also prove that a subsingleton family is always independent and that an independent family implies the measure is a probability measure. This latter result means we can drop IsProbabilityMeasure μ assumptions from many theorems. From PFR