Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-03-03 17:42
c08143f5
View on Github →
feat: more versions of the characteristic function of a sum (
#36058
)
Estimated changes
Modified
Mathlib/Probability/Independence/CharacteristicFunction.lean
added
theorem
ProbabilityTheory.IndepFun.charFunDual_map_fun_add_eq_mul
added
theorem
ProbabilityTheory.IndepFun.charFun_map_fun_add_eq_mul
added
theorem
ProbabilityTheory.charFunDual_map_add_prod_eq_mul
added
theorem
ProbabilityTheory.charFunDual_map_sum_pi_eq_prod
added
theorem
ProbabilityTheory.charFun_map_add_prod_eq_mul
added
theorem
ProbabilityTheory.charFun_map_sum_pi_eq_prod
added
theorem
ProbabilityTheory.iIndepFun.charFunDual_map_fun_sum_eq_prod
added
theorem
ProbabilityTheory.iIndepFun.charFun_map_fun_sum_eq_prod