associated_iff_eq — Mathlib

English

In a monoid with units that form a singleton, two elements are associated if and only if they are equal.

Русский

В моноиде с единицами, образующими единичную группу, два элемента ассоциированы тогда и только тогда, когда они равны.

LaTeX

$$$$\forall x,y \in M,\ x \sim y \iff x = y,$$ with [Monoid M] and [Subsingleton M^×].$$

Lean4

theorem associated_iff_eq {x y : M} : x ~ᵤ y ↔ x = y :=
  by
  constructor
  · rintro ⟨c, rfl⟩
    rw [units_eq_one c, Units.val_one, mul_one]
  · rintro rfl
    rfl

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