Def real.of_rat
Modification history
2022-07-21 16:19
src/data/real/basic.lean
chore(data/real/basic,number_theory/padics/padic_numbers): eliminate `real.of_rat` and `padic.of_rat` (#15569) …
Deleted real.of_ratView on Github →2021-02-04 21:33
src/data/real/basic.lean
refactor(data/real/basic): make ℝ a structure (#6024) …
Modified real.of_ratView on Github →2020-04-17 16:30
src/data/real/basic.lean
chore(*): migrate `nat/int/rat.eq_cast` to bundled homs (#2427) …
Modified real.of_ratView on Github →2018-08-21 22:05
data/real/basic.lean
refactor(data/real/nnreal): derive order structure for ennreal from with_top nnreal
Modified real.of_ratView on Github →2018-08-16 11:23
data/real/basic.lean
feat(data/padics): p-adic numbers (#262)
Modified real.of_ratView on Github →