Theorem Set.Iio_mul_bij

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.Iio_mul_bijView on Github →