mem_transferSet

Mathlib.GroupTheory.Transfer

URI: https://scilib.ai/kg/mathlib#Subgroup.mem_transferSet

English

For any q in G/H, the value transferFunction(H,g,q) lies inside the transferSet(H,g).

Русский

Для любой косеты q в G/H значение transferFunction(H,g,q) лежит в transferSet(H,g).

LaTeX

$$$\operatorname{transferFunction}(H,g,q) \in \operatorname{transferSet}(H,g)$$$

Lean4

theorem mem_transferSet (q : G ⧸ H) : transferFunction H g q ∈ transferSet H g :=
  ⟨q, rfl⟩

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

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

Разделы

Аффилиация

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