instIsSymm

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associated.instIsSymm

English

There is an IsSymm instance for Associated on any monoid.

Русский

Для Associated на любом моноиде существует инстанс IsSymm.

LaTeX

$$$\\forall x,y\\, Associated x y \\Rightarrow Associated y x$$$

Lean4

instance [Monoid M] : IsSymm M Associated :=
  ⟨fun _ _ => Associated.symm⟩

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

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

Разделы

Аффилиация

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