mathlib
a8076b2c - refactor(data/real/irrational): review (#2304)

Commit
5 years ago
refactor(data/real/irrational): review (#2304) * refactor(data/real/irrational): review * Update src/data/real/irrational.lean * Update src/data/real/irrational.lean * Apply suggestions from code review Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading