Theorems · Theorem · order theory

min_mul_distrib

∀ {α : Type u} [inst : Monoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedMul α] (a b c : α),
  min a (b * c) = min a (min a b * min a c)

Defined in

Mathlib.Algebra.Order.Monoid.Canonical.Defs

Cited by

1 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

MonoidLinearOrderCanonicallyOrderedMul