Theorem ProbabilityTheory.IndepFun.charFun_map_fun_add_eq_mul

Modification history

2026-03-03 17:42
Mathlib/Probability/Independence/CharacteristicFunction.lean
feat: more versions of the characteristic function of a sum (#36058)
Added ProbabilityTheory.IndepFun.charFun_map_fun_add_eq_mulView on Github →