Theorem ProbabilityTheory.iIndepFun.charFun_map_finsetSum_eq_prod

Modification history

2026-04-26 16:26
Mathlib/Probability/Independence/CharacteristicFunction.lean
chore: camel-case `finset_sum` in lemma names (#37793) …
Added ProbabilityTheory.iIndepFun.charFun_map_finsetSum_eq_prodView on Github →