Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-03 14:28 81120aec

View on Github →

refactor(number_theory): reorganize number field results into new subfolder (#16764)

  • 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

Estimated changes

added theorem int.not_is_field
deleted theorem int.not_is_field