max_mul_min — Mathlib

English

Let α be a linearly ordered set with a commutative multiplication. Then for all a, b ∈ α, max(a, b) · min(a, b) = a · b.

Русский

Пусть α упорядочено линейно, и операция умножения коммутативна. Тогда для любых a, b ∈ α выполняется max(a, b) · min(a, b) = a · b.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem max_mul_min (a b : α) : max a b * min a b = a * b :=
  fn_max_mul_fn_min id _ _

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