Theorem ProbabilityTheory.covariance_mul_left

Modification history

2025-12-03 18:57
Mathlib/Probability/Moments/Covariance.lean
feat: covariance of a variable multiplied by a constant (#32234) …
Deleted ProbabilityTheory.covariance_mul_leftView on Github →
2025-08-01 21:30
Mathlib/Probability/Moments/Covariance.lean
chore: tidy various files (#27630)
Modified ProbabilityTheory.covariance_mul_leftView on Github →
2025-07-26 14:42
Mathlib/Probability/Moments/Covariance.lean
feat(Probability): covariance of sums and maps (#26998) …
Added ProbabilityTheory.covariance_mul_leftView on Github →