associated_eq_eq — Mathlib

English

The relation of association coincides with equality under the given subsingleton units assumption.

Русский

Отношение ассоциации совпадает с равенством при условии подмножества единиц.

LaTeX

$$$$\mathrm{Associated} = \mathrm{Eq}$$ in the presence of [Monoid M] and [Subsingleton (Units M)].$$

Lean4

theorem associated_eq_eq : (Associated : M → M → Prop) = Eq :=
  by
  ext
  rw [associated_iff_eq]

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