Theorems · Theorem · order theory

Set.Iio_mul_bij

∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  Set.BijOn (fun x => x * a) (Set.Iio b) (Set.Iio (b * a))

Defined in

Mathlib.Algebra.Order.Group.Pointwise.Interval

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommGroupPartialOrderIsOrderedMonoid