mathlib

b7148c4e - feat(analysis/special_functions/pow): Rational powers are dense (#15002)

feat(analysis/special_functions/pow): Rational powers are dense (#15002) There is a rational square between any two positive elements of an archimedean ordered field. Co-authored-by: Alex Best <alex.j.best@gmail.com>