Commit 2026-01-29 16:43 f821781e

View on Github →

feat(Algebra/Order): multiplicative versions of lemmas on (pre)images of intervals under group operations (#34561) Currently, Mathlib/Algebra/Order/Group/Pointwise/Interval.lean contains lemmas about (pre)images of intervals under group operations only for additive groups. This PR adds multiplicative versions and derives the additive ones via to_additive. It also renames lemmas about GroupWithZero (e.g. preimage_const_mul_Ico → preimage_const_mul_Ico₀) to avoid name collisions.

Estimated changes

deleted theorem Set.Iic_add_bij
added theorem Set.Iic_mul_bij
deleted theorem Set.Iio_add_bij
added theorem Set.Iio_mul_bij
deleted theorem Set.image_add_const_Iic
deleted theorem Set.image_add_const_Iio
deleted theorem Set.image_const_add_Iic
deleted theorem Set.image_const_add_Iio
deleted theorem Set.image_const_sub_Icc
deleted theorem Set.image_const_sub_Ici
deleted theorem Set.image_const_sub_Ico
deleted theorem Set.image_const_sub_Iic
deleted theorem Set.image_const_sub_Iio
deleted theorem Set.image_const_sub_Ioc
deleted theorem Set.image_const_sub_Ioi
deleted theorem Set.image_const_sub_Ioo
added theorem Set.image_inv_Icc
added theorem Set.image_inv_Ici
added theorem Set.image_inv_Ico
added theorem Set.image_inv_Iic
added theorem Set.image_inv_Iio
added theorem Set.image_inv_Ioc
added theorem Set.image_inv_Ioi
added theorem Set.image_inv_Ioo
deleted theorem Set.image_neg_Icc
deleted theorem Set.image_neg_Ici
deleted theorem Set.image_neg_Ico
deleted theorem Set.image_neg_Iic
deleted theorem Set.image_neg_Iio
deleted theorem Set.image_neg_Ioc
deleted theorem Set.image_neg_Ioi
deleted theorem Set.image_neg_Ioo
deleted theorem Set.image_sub_const_Icc
deleted theorem Set.image_sub_const_Ici
deleted theorem Set.image_sub_const_Ico
deleted theorem Set.image_sub_const_Iic
deleted theorem Set.image_sub_const_Iio
deleted theorem Set.image_sub_const_Ioc
deleted theorem Set.image_sub_const_Ioi
deleted theorem Set.image_sub_const_Ioo
modified theorem Set.preimage_const_mul_Icc
modified theorem Set.preimage_const_mul_Ici
modified theorem Set.preimage_const_mul_Ico
modified theorem Set.preimage_const_mul_Iic
modified theorem Set.preimage_const_mul_Iio
modified theorem Set.preimage_const_mul_Ioc
modified theorem Set.preimage_const_mul_Ioi
modified theorem Set.preimage_const_mul_Ioo
modified theorem Set.preimage_mul_const_Icc
modified theorem Set.preimage_mul_const_Ici
modified theorem Set.preimage_mul_const_Ico
modified theorem Set.preimage_mul_const_Iic
modified theorem Set.preimage_mul_const_Iio
modified theorem Set.preimage_mul_const_Ioc
modified theorem Set.preimage_mul_const_Ioi
modified theorem Set.preimage_mul_const_Ioo