comm

Mathlib.Algebra.GroupWithZero.Associated

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

English

Associated is symmetric: x ~ᵤ y iff y ~ᵤ x.

Русский

Связанность симметрична: x ~ᵤ y ⇔ y ~ᵤ x.

LaTeX

$$$\\forall \\{x,y:M\\}, x ~ᵤ y \\iff y ~ᵤ x$$$

Lean4

protected theorem comm [Monoid M] {x y : M} : x ~ᵤ y ↔ y ~ᵤ x :=
  ⟨Associated.symm, Associated.symm⟩

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

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

Разделы

Аффилиация

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