Zulip Chat Archive

Stream: general

Topic: Refactor number_field

Xavier Roblot (Oct 02 2022 at 16:44):

I would like to suggest the following refactor of number_field.

  • Create a new dir number_field in number_theory
  • Move the current file number_field.lean to number_theory/number_field/basic.lean
  • Move the results about embeddings from this file to a new file number_theory/number_field/embeddings.lean
  • Move the file number_theory/class_number/number_field.lean to number_theory/number_field/class_number.lean

There might some other files that would need to move to the new dir. The PR is #16764.

I am pinging the authors of all the files concerned for their opinion @Riccardo Brasca @Anne Baanen @Ashvni Narayanan @Alex J. Best

Riccardo Brasca (Oct 02 2022 at 16:45):

I am totally in favor of splitting number_field.

Ashvni Narayanan (Oct 02 2022 at 16:47):

That seems fine

Filippo A. E. Nuccio (Oct 03 2022 at 07:57):

I certainly agree.

Last updated: Dec 20 2023 at 11:08 UTC