associated_abs_left_iff — Mathlib

English

In a ring with order, the associate relation respects taking absolute values on the left: Associated |x| y if and only if Associated x y.

Русский

В кольце с порядком отношение ассоциированности сохраняется при взятии модуля слева: Associated |x| y ⇔ Associated x y.

LaTeX

$$Associated |x| y \Leftrightarrow Associated x y$$

Lean4

@[simp]
theorem associated_abs_left_iff : Associated |x| y ↔ Associated x y := by obtain h | h := abs_choice x <;> simp [h]

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