symm

Mathlib.Algebra.GroupWithZero.Associated

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

English

If x is associated to y, then y is associated to x.

Русский

Если x ассоциировано с y, то y ассоциировано с x.

LaTeX

$$$ x ~ᵤ y \\rightarrow y ~ᵤ x. $$$

Lean4

@[symm]
protected theorem symm [Monoid M] : ∀ {x y : M}, x ~ᵤ y → y ~ᵤ x
  | x, _, ⟨u, rfl⟩ => ⟨u⁻¹, by rw [mul_assoc, Units.mul_inv, mul_one]⟩

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

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

Разделы

Аффилиация

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