Commit 2020-08-13 14:29 c66ecd3f

View on Github →

feat(intervals/image_preimage): preimage under multiplication (#3757) Add lemmas preimage_mul_const_Ixx and preimage_const_mul_Ixx. Also generalize equiv.mul_left and equiv.mul_right to units.

Estimated changes

Modified src/algebra/ordered_field.lean

added theorem lt_div_iff_of_neg

Modified src/data/equiv/mul_add.lean

modified def to_units

added theorem units.coe_mul_left

added theorem units.coe_mul_right

added def units.mul_left

added theorem units.mul_left_symm

added def units.mul_right

added theorem units.mul_right_symm

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

added theorem set.preimage_const_mul_Icc

added theorem set.preimage_const_mul_Icc_of_neg

added theorem set.preimage_const_mul_Ici

added theorem set.preimage_const_mul_Ici_of_neg

added theorem set.preimage_const_mul_Ico

added theorem set.preimage_const_mul_Ico_of_neg

added theorem set.preimage_const_mul_Iic

added theorem set.preimage_const_mul_Iic_of_neg

added theorem set.preimage_const_mul_Iio

added theorem set.preimage_const_mul_Iio_of_neg

added theorem set.preimage_const_mul_Ioc

added theorem set.preimage_const_mul_Ioc_of_neg

added theorem set.preimage_const_mul_Ioi

added theorem set.preimage_const_mul_Ioi_of_neg

added theorem set.preimage_const_mul_Ioo

added theorem set.preimage_const_mul_Ioo_of_neg

added theorem set.preimage_mul_const_Icc

added theorem set.preimage_mul_const_Icc_of_neg

added theorem set.preimage_mul_const_Ici

added theorem set.preimage_mul_const_Ici_of_neg

added theorem set.preimage_mul_const_Ico

added theorem set.preimage_mul_const_Ico_of_neg

added theorem set.preimage_mul_const_Iic

added theorem set.preimage_mul_const_Iic_of_neg

added theorem set.preimage_mul_const_Iio

added theorem set.preimage_mul_const_Iio_of_neg

added theorem set.preimage_mul_const_Ioc

added theorem set.preimage_mul_const_Ioc_of_neg

added theorem set.preimage_mul_const_Ioi

added theorem set.preimage_mul_const_Ioi_of_neg

added theorem set.preimage_mul_const_Ioo

added theorem set.preimage_mul_const_Ioo_of_neg

Modified src/dynamics/circle/rotation_number/translation_number.lean

Modified src/group_theory/group_action.lean