chore(number_theory/number_field/basic): fix a name (#16943)
chore(number_theory/number_field/basic): fix a name (#16943)

This lemma is in the `ring_of_integers` namespace, so the name was redundant.





leanprover-community/mathlib,leanprover-community/mathlib