rfl

Mathlib.Algebra.GroupWithZero.Associated

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

English

The relation is reflexive on any monoid.

Русский

Отношение ассоциированности рефлексивно на любом моноиде.

LaTeX

$$$ \\forall x \\in M, \\ x ~ᵤ x. $$$

Lean4

protected theorem rfl [Monoid M] {x : M} : x ~ᵤ x :=
  .refl x

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

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

Разделы

Аффилиация

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