Theorem ProbabilityTheory.HasGaussianLaw.prodMk

Modification history

2026-01-26 14:59

Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean

feat: add a predicate HasGaussianLaw (#32144) …

Added ProbabilityTheory.HasGaussianLaw.prodMk View on Github →