Commit 2021-10-14 07:51 264ff903
View on Github →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