Add import to existing mathlib file or create a new one?

Stream: general

[Michael Stoll]

In #14572 there is a couple of definitions/lemmas that should be moved (like the other stuff currently in number_theory/legendre_symbol/auxiliary.lean) to a good place in mathlib. In this case, both algebra.trace and field_theory.finite.basic seem to be reasonable; the two statements (the last two in auxiliary.lean as in the PR) refer to definitions from both files. But neither of these two files already imports the other (I checked that definitions from the other file are unknown in each file). So if I move the statements to one of these files, I'd have to add the import of the other file. Alternatively, I could set up a new file, say field_theory.finite.trace to contain the two, which imports the other two files.

What would be the preferred way to proceed?

I noticed that there are files in mathlib that contain only very few statements (in some cases, only one), so that seems to be OK.

[Alex J. Best]

I think that is the usual way to proceed yes. Unless there is some other file in field_theory/finite that already imports basic and algebra.trace for some reason a new file seems appropriate in this situation

[Michael Stoll]

OK, thanks.
The other two files in field_theory/finite do not import algebra.trace, so I'll go for the new file.