instIsRefl

Mathlib.Algebra.Group.Commute.Defs

URI: https://scilib.ai/kg/mathlib#Commute.instIsRefl

English

The relation Commute is reflexive.

Русский

Отношение Commute рефлексивно.

LaTeX

$$$\\forall S [Mul S],\\ IsRefl S Commute$$$

Lean4

@[to_additive]
instance : IsRefl S Commute :=
  ⟨Commute.refl⟩
    -- This instance is useful for `Finset.noncommProd`

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

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

Разделы

Аффилиация

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