[Merged by Bors] - feat: if a sigma-algebra is independent from itself then all sets in it have measure 0 or 1#39750

mathlib-splicebot[bot] wants to merge 3 commits into

masterleanprover-community/mathlib4:masterfrom

splice-bot/pr-37259-Mathlib-Probability-Independence-ZeroOne.lean-1106d86409-k7j2uz0leanprover-community/mathlib4_copy:splice-bot/pr-37259-Mathlib-Probability-Independence-ZeroOne.lean-1106d86409-k7j2uz0Copy head branch name to clipboard