Commit 2025-04-22 08:56 ef91d94f

View on Github →

chore(Group/Pointwise/Interval): generalize some lemmas (#23857) .. from a linear ordered field to a linear ordered semifield or a group with zero.

Estimated changes

modified theorem Set.image_mul_left_Icc'
modified theorem Set.image_mul_left_Icc
added theorem Set.image_mul_left_Ici
modified theorem Set.image_mul_left_Ico
added theorem Set.image_mul_left_Iic
added theorem Set.image_mul_left_Iio
modified theorem Set.image_mul_left_Ioc
added theorem Set.image_mul_left_Ioi
modified theorem Set.image_mul_left_Ioo
modified theorem Set.image_mul_right_Icc'
modified theorem Set.image_mul_right_Icc
modified theorem Set.image_mul_right_Ico
modified theorem Set.image_mul_right_Ioc
modified theorem Set.image_mul_right_Ioo
modified theorem Set.inv_Ioi₀
modified theorem Set.inv_Ioo_0_left
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