conjugatesOf

Mathlib.Algebra.Group.Conj

URI: https://scilib.ai/kg/mathlib#conjugatesOf

English

The set conjugatesOf(a) consists of all b such that IsConj(a,b).

Русский

Множество conjugatesOf(a) состоит из всех b, для которых IsConj(a,b).

LaTeX

$$$\mathrm{conjugatesOf}(a) = \{b \in \alpha \mid IsConj(a,b)\}$$$

Lean4

/-- Given an element `a`, `conjugatesOf a` is the set of conjugates. -/
def conjugatesOf (a : α) : Set α :=
  {b | IsConj a b}

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

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

Разделы

Аффилиация

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