setoid

Mathlib.GroupTheory.DoubleCoset

URI: https://scilib.ai/kg/mathlib#DoubleCoset.setoid

English

The setoid on G is defined by the kernel of x ↦ doubleCoset x H K.

Русский

Множество отношения на G задано как ядро отображения x ↦ doubleCoset x H K.

LaTeX

$$$ \\text{setoid}(H,K) : Setoid(G) = \\mathrm{Setoid.ker}(x \\mapsto \\mathrm{doubleCoset}(x,H,K)) $$$

Lean4

/-- The setoid defined by the double_coset relation -/
def setoid (H K : Set G) : Setoid G :=
  Setoid.ker fun x => doubleCoset x H K

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

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

Разделы

Аффилиация

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