mathlib

0bea64b5 - feat(ring_theory/integrally_closed): if x is in Frac R such that x^n is in R then x is in R (#12812)