basic): fix a name (#16943)

Commit

3 years ago

chore(number_theory/number_field/basic): fix a name (#16943) This lemma is in the `ring_of_integers` namespace, so the name was redundant.

Author

riccardobrasca

Parents