Theorem Set.preimage_const_mul_Icc₀

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.preimage_const_mul_Icc₀View on Github →