mathlib3
c66ecd3f - feat(intervals/image_preimage): preimage under multiplication (#3757)

Commit
5 years ago
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`.
Author
Parents
Loading