Theorem ProbabilityTheory.HasGaussianLaw.toLp_pi

Modification history

2026-04-13 23:01
Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean
perf(Analysis/Normed/Group): lower instance priorities (#37962) …
Modified ProbabilityTheory.HasGaussianLaw.toLp_piView on Github →
2026-01-26 14:59
Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean
feat: add a predicate HasGaussianLaw (#32144) …
Added ProbabilityTheory.HasGaussianLaw.toLp_piView on Github →