English
Let G be a linearly ordered group and H a subgroup of G closed under inversion. Then for every x in G, the multiplicative absolute value |x| is in H if and only if x is in H.
Русский
Пусть G — линейно упорядоченная группа, и H — подпгруппа G, замкнутая относительно инверсии. Тогда для любого x ∈ G выполнено: |x| ∈ H тогда и только если x ∈ H.
LaTeX
$$$|x|_m \in H \iff x \in H$$$
Lean4
@[to_additive (attr := simp)]
theorem mabs_mem_iff {S G} [Group G] [LinearOrder G] {_ : SetLike S G} [InvMemClass S G] {H : S} {x : G} :
|x|ₘ ∈ H ↔ x ∈ H := by cases mabs_choice x <;> simp [*]