Zulip Chat Archive

Stream: general

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

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 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 (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 basic and algebra.trace for some reason a new file seems appropriate in this situation

Michael Stoll (Jun 09 2022 at 18:52):

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

Last updated: Dec 20 2023 at 11:08 UTC