Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-13 11:47 29761083

View on Github →

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

Estimated changes