Theorems · Theorem · order theory

Set.smul_Icc

∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] [MulLeftReflectLE α]
  [ExistsMulOfLE α] (a b c : α), a • Set.Icc b c = Set.Icc (a * b) (a * c)

Defined in

Mathlib.Algebra.Order.Group.Pointwise.Interval

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

CommMonoidLinearOrderIsOrderedMonoidMulLeftReflectLEExistsMulOfLE