mathlib

3b9e2ef2 - feat(data/real/sqrt): add sqrt_div' lemma (#18216)

feat(data/real/sqrt): add sqrt_div' lemma (#18216) The current sqrt_div lemma requires the numerator to be non-negative. It is also sufficient to have the denominator be non-negative. This matches how we have both `sqrt_mul` and `sqrt_mul'`.