mk_eq_mk_iff_associated

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.mk_eq_mk_iff_associated

English

Equality of representatives in Associates corresponds to associativity.

Русский

Равенство представителей в Associates соответствует ассоциированности.

LaTeX

$$$$\ Associates.mk a = Associates.mk b \iff a \sim_{\mathrm{a}} b.$$$$

Lean4

theorem mk_eq_mk_iff_associated [Monoid M] {a b : M} : Associates.mk a = Associates.mk b ↔ a ~ᵤ b :=
  Iff.intro Quotient.exact Quot.sound

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru