Theorem ProbabilityTheory.iIndepFun.charFun_map_fun_sum_eq_prod

Modification history

2026-03-06 11:44
Mathlib/Probability/Independence/CharacteristicFunction.lean
feat: lemmas about characteristic function (#36251) …
Modified ProbabilityTheory.iIndepFun.charFun_map_fun_sum_eq_prodView on Github →
2026-03-03 17:42
Mathlib/Probability/Independence/CharacteristicFunction.lean
feat: more versions of the characteristic function of a sum (#36058)
Added ProbabilityTheory.iIndepFun.charFun_map_fun_sum_eq_prodView on Github →