Theorem Set.image_const_mul_Iio

Modification history

2026-01-29 16:43
Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
feat(Algebra/Order): multiplicative versions of lemmas on (pre)images of intervals under group operations (#34561) …
Added Set.image_const_mul_IioView on Github →