Mathlib v3 is deprecated. Go to Mathlib v4

Theorem probability_theory.ident_distrib.const_mul

Modification history

2022-05-08 12:55
src/probability/ident_distrib.lean
feat(probability/ident_distrib): identically distributed random variables (#14024)
Added probability_theory.ident_distrib.const_mulView on Github →