Where to put a lemma proving property X about Y?

Stream: mathlib4

[Vasily Ilin]

Say, I prove property X about Y. Where in mathlib do I put this theorem, in the file containing X or the file containing Y or a new file? In my case, X is a moment-generating function and Y is a Gaussian distribution.
https://github.com/leanprover-community/mathlib4/pull/19886

[Johan Commelin]

@Vasily Ilin You could create a new file with

import Mathlib

-- your lemma

#find_home! your_lemma_name

Hopefully that will give you a good suggestion.

[Johan Commelin]

In general, I don't think we have a strong rule about this scenario. We try to take into account how to optimize the import structure.

[Kim Morrison]

But don't be too afraid to make new files. :-)