mathlib3
78252a30 - chore(data/real/sqrt): A couple of lemmas about sqrt (#9892)

Commit
4 years ago
chore(data/real/sqrt): A couple of lemmas about sqrt (#9892) Add a couple of lemmas about `sqrt x / x`.
Author
Parents
Loading