min_mul_mul_right — Mathlib

English

Let α be a linearly ordered set with Mul α and MulRightMono α. Then for all a, b, c ∈ α, min(a·c, b·c) = min(a, b) · c.

Русский

Пусть α упорядочено линейно и есть умножение справа. Тогда min(a·c, b·c) = min(a, b) · c.

LaTeX

$$$ \min(a c, b c) = \min(a,b) \cdot c $$$

Lean4

@[to_additive]
theorem min_mul_mul_right (a b c : α) : min (a * c) (b * c) = min a b * c :=
  (monotone_id.mul_const' c).map_min.symm

Похожие утверждения