Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-08 11:22 fb22ae33

View on Github →

refactor(order/rel_iso): move statements about intervals to data/set/intervals (#8150) This means that we can talk about rel_iso without needing to transitively import ordered_groups This PR takes advantage of this to define order_iso.mul_(left|right)['] to mirror equiv.mul_(left|right)['].

Estimated changes

Modified src/algebra/ordered_field.lean

added def order_iso.mul_left'

added def order_iso.mul_right'

Modified src/algebra/ordered_group.lean

added def order_iso.mul_left

added def order_iso.mul_right

Modified src/data/set/intervals/basic.lean

added def order_iso.Ici_bot

added def order_iso.Iic_top

added theorem order_iso.preimage_Icc

added theorem order_iso.preimage_Ici

added theorem order_iso.preimage_Ico

added theorem order_iso.preimage_Iic

added theorem order_iso.preimage_Iio

added theorem order_iso.preimage_Ioc

added theorem order_iso.preimage_Ioi

added theorem order_iso.preimage_Ioo

Modified src/order/rel_iso.lean

deleted def order_iso.Ici_bot

deleted def order_iso.Iic_top

deleted theorem order_iso.preimage_Icc

deleted theorem order_iso.preimage_Ici

deleted theorem order_iso.preimage_Ico

deleted theorem order_iso.preimage_Iic

deleted theorem order_iso.preimage_Iio

deleted theorem order_iso.preimage_Ioc

deleted theorem order_iso.preimage_Ioi

deleted theorem order_iso.preimage_Ioo