identDistrib and hasLaw

Stream: Is there code for X?

[Joris van Winden]

Is there a theorem which says that if two functions have the same law (via ProbabilityTheory.HasLaw), then the functions have the same distribution (via ProbabilityTheory.IdentDistrib)?

I found no results when combining the mentioned types in loogle.

[Etienne Marion]

@loogle ProbabilityTheory.IdentDistrib, ProbabilityTheory.HasLaw

[loogle]

:shrug: nothing found

[Etienne Marion]

No there isn't.

[Joris van Winden]

Would it be nice to have in mathlib? I think the proof should be easy.

[Joris van Winden]

#34844 feat(Probability/IdentDistrib): add of_hasLaw lemma