Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ivl_translate

Modification history

2019-12-15 22:29

src/algebra/ordered_field.lean

feat(data/set/intervals): add `nonempty_Icc` etc, `image_(add/mul)_(left/right)_Icc` (#1803)

Deleted ivl_translate View on Github →

2018-01-14 21:59

algebra/field.lean

feat(algebra/field): more division lemmas

Modified ivl_translate View on Github →

2017-08-10 16:36

algebra/field.lean

construct reals as complete, linear ordered field

Added ivl_translate View on Github →