English
Let G be a commutative ordered group with IsOrderedMonoid structure. For a, b in G, the multiplicative absolute value satisfies |ab|_m = |a|_m |b|_m if and only if either both a and b are at least 1, or both are at most 1.
Русский
Пусть G — коммутативная упорядоченная группа с упорядоченной моноидальной структурой. Для a, b в G верно: |ab|_м = |a|_м |b|_м тогда и только тогда, когда либо оба a и b не меньше 1, либо оба не больше 1.
LaTeX
$$$|ab|_m = |a|_m \;|b|_m \quad\iff\quad (1 \le a \land 1 \le b) \lor (a \le 1 \land b \le 1).$$$
Lean4
@[to_additive]
theorem mabs_mul_eq_mul_mabs_iff (a b : G) : |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1 :=
by
obtain ab | ab := le_total a b
· exact mabs_mul_eq_mul_mabs_le ab
· simpa only [mul_comm, and_comm] using mabs_mul_eq_mul_mabs_le ab
