Theorem ProbabilityTheory.isGaussian_map_equiv_iff

Modification history

2025-05-16 10:47
Mathlib/Probability/Distributions/Gaussian/Basic.lean
feat: define Gaussian measures in normed spaces (#24900) …
Added ProbabilityTheory.isGaussian_map_equiv_iffView on Github →