mathlib

264ff903 - refactor(analysis/special_functions): generalise nth-root lemmas (#9704)

refactor(analysis/special_functions): generalise nth-root lemmas (#9704) `exists_pow_nat_eq` and `exists_eq_mul_self` both hold for any algebraically closed field, so pull them out into `is_alg_closed/basic` and generalise appropriately Closes #4674