Michael Stoll (Jun 09 2022 at 18:19):
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
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 (Jun 09 2022 at 18:50):
I think that is the usual way to proceed yes. Unless there is some other file in
field_theory/finite that already imports
algebra.trace for some reason a new file seems appropriate in this situation
Michael Stoll (Jun 09 2022 at 18:52):
The other two files in
field_theory/finite do not import
algebra.trace, so I'll go for the new file.
Last updated: Aug 03 2023 at 10:10 UTC