Associated — Mathlib

English

Two elements x,y of a monoid M are associated iff there exists a unit u with x u = y.

Русский

Два элемента x,y моноида M связаны отношением ассоциированности, если существует единица u такая, что x u = y.

LaTeX

$$$ x ~ᵤ y \\iff \\exists u \\in M^{\\times},\\ x u = y. $$$

Lean4

/-- Two elements of a `Monoid` are `Associated` if one of them is another one
multiplied by a unit on the right. -/
def Associated [Monoid M] (x y : M) : Prop :=
  ∃ u : Mˣ, x * u = y

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