refl

Mathlib.Algebra.Group.Conj

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

English

IsConj(a,a) holds for any a.

Русский

Для любого a выполняется IsConj(a,a).

LaTeX

$$$IsConj(a,a)$$$

Lean4

@[refl]
theorem refl (a : α) : IsConj a a :=
  ⟨1, SemiconjBy.one_left a⟩

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

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

Разделы

Аффилиация

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