Commit 2025-08-01 13:58 8c87ce1b

chore: define covariance before variance (#27736) Make the variance file import covariance instead of the other way around. That way we can for instance prove first that the covariance of independent random variables is 0 to then deduce that the variance of a sum of independent random variables is the sum of their variances (done in #27749).