refl

Mathlib.Algebra.GroupWithZero.Associated

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

English

Every element is associated with itself in a monoid.

Русский

Каждый элемент ассоциирован с самим собой в моноиде.

LaTeX

$$$ x ~ᵤ x. $$$

Lean4

@[refl]
protected theorem refl [Monoid M] (x : M) : x ~ᵤ x :=
  ⟨1, by simp⟩

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

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

Разделы

Аффилиация

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