Theorem ProbabilityTheory.moment_def

Modification history

2025-09-23 11:51

Mathlib/Probability/Moments/Basic.lean

feat(ProbabilityTheory): Add `moment_def` and `moment_one` (#29902) …

Added ProbabilityTheory.moment_def View on Github →