mathlib3

39014ec9 - feat(probability/independence): add indep_bot_left and indep_bot_right (#16309)

feat(probability/independence): add indep_bot_left and indep_bot_right (#16309) Prove that for any `m`, `indep m ⊥ μ`, and prove the corresponding statement with bot on the left. Also declare two types as variables on top of the file and remove them from many lemmas.