mabs_mem_iff — Mathlib

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 [*]

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