mabs_mul_three — Mathlib

English

In a linearly ordered commutative group, the multiplicative absolute value of a product does not exceed the product of multiplicative absolute values: |a b c|_m ≤ |a|_m |b|_m |c|_m.

Русский

В линейно упорядоченной коммутативной группе: |a b c|ₘ ≤ |a|ₘ |b|ₘ |c|ₘ.

LaTeX

$$$|a b c|_m \le |a|_m \;|b|_m \;|c|_m$$$

Lean4

@[to_additive]
theorem mabs_mul_three (a b c : G) : |a * b * c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ :=
  (mabs_mul_le _ _).trans (mul_le_mul_right' (mabs_mul_le _ _) _)

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