Associates — Mathlib

English

The Associates M is the quotient of M by the Associated relation.

Русский

Associates M есть фактор-мой не по отношению к ассоциации в M.

LaTeX

$$$$\text{Associates } M \;=\; \text{Quotient}(\mathrm{Associated.setoid}\, M).$$$$

Lean4

/-- The quotient of a monoid by the `Associated` relation. Two elements `x` and `y`
  are associated iff there is a unit `u` such that `x * u = y`. There is a natural
  monoid structure on `Associates M`. -/
abbrev Associates (M : Type*) [Monoid M] : Type _ :=
  Quotient (Associated.setoid M)

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