Commit 2024-05-18 16:15 57e4f13b

View on Github →

feat(Probability/Independence): add IndepFun.neg (#13000) In order to enhance findability we have added:

IndepFun.neg_right
IndepFun.neg_left Co-Authored-By: Lorenzo Luccioli 71074618+LorenzoLuccioli@users.noreply.github.com

Estimated changes

Modified Mathlib/Probability/Independence/Basic.lean

added theorem ProbabilityTheory.IndepFun.neg_left

added theorem ProbabilityTheory.IndepFun.neg_right

Modified Mathlib/Probability/Independence/Conditional.lean

added theorem ProbabilityTheory.CondIndepFun.neg_left

added theorem ProbabilityTheory.CondIndepFun.neg_right

Modified Mathlib/Probability/Independence/Kernel.lean

added theorem ProbabilityTheory.kernel.IndepFun.neg_left

added theorem ProbabilityTheory.kernel.IndepFun.neg_right