Commit 2019-05-07 19:03 820bac36
View on Github →building the hyperreal library (#835)
- more instances
- fix stuff that got weirded
- fix stuff that got weird
- fix stuff that became weird
- build hyperreal library (with sorries)
- fix weirdness, prettify etc.
- spaces
- st lt le lemmas fix type
- Update src/data/real/hyperreal.lean Co-Authored-By: abhimanyupallavisudhir 43954672+abhimanyupallavisudhir@users.noreply.github.com
- if then
- more stuff
- Update hyperreal.lean
- Update hyperreal.lean
- Update basic.lean
- Update basic.lean
- Update hyperreal.lean
- of_max, of_min, of_abs
- Update filter_product.lean
- Update hyperreal.lean
- abs_def etc.
- Update filter_product.lean
- hole
- Update hyperreal.lean
- Update filter_product.lean
- Update filter_product.lean
- Update filter_product.lean
- Update hyperreal.lean
- Update hyperreal.lean
- Update filter_product.lean
- Update hyperreal.lean
- Update hyperreal.lean
- finally done with all sorries!
- Update hyperreal.lean
- fix (?)
- fix (?) ring issue
- real.Sup_univ
- st is Sup
- st_id_real spacebar
- sup --> Sup
- fix weirds
- dollar signs
- 100-column
- 100 columns rule
- Update hyperreal.lean
- removing uparrows
- uparrows
- some stuff that got away
- fix
- lift_id
- fix?
- fix mono, hopefully
- fix mono, hopefully
- this should work
- fix -- no more mono
- fixes
- fixes
- fixes
- fixes
- ok, fixed