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 _ _) _)