max_mul_mul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem max_mul_mul_right (a b c : α) : max (a * c) (b * c) = max a b * c :=
  (monotone_id.mul_const' c).map_max.symm

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