mathlib3

9728bd25 - chore(number_theory/number_field): golf `int.not_is_field` (#12451)

chore(number_theory/number_field): golf `int.not_is_field` (#12451) Golfed proof of number_theory.number_field.int.not_is_field Co-authored by: David Ang <dka31@cantab.ac.uk> Co-authored by: Eric Rodriguez <ericrboidi@gmail.com> Co-authored by: Violeta Hernández <vi.hdz.p@gmail.com> Co-authored-by: Aresh-P <91763341+Aresh-P@users.noreply.github.com>