Commit 2025-12-03 18:57 e9259fab

feat: covariance of a variable multiplied by a constant (#32234) Rename covariance_mul_left : cov[fun ω ↦ c * X ω, Y; μ] = c * cov[X, Y; μ] to covariance_const_mul_left and add covariance_mul_const_left : cov[fun ω ↦ X ω * c, Y; μ] = cov[X, Y; μ] * c. Same for right and variance. Also minimize the public imports in the Covariance file.