orbit

Mathlib.GroupTheory.GroupAction.Blocks

URI: https://scilib.ai/kg/mathlib#MulAction.IsFixedBlock.orbit

← MathLib Explorer

English

An orbit is a fixed block: IsFixedBlock G (orbit G a).

Русский

Орбита является фиксированным блоком: IsFixedBlock G (orbit G a).

LaTeX

$$$ \\text{IsFixedBlock } G (\\mathrm{orbit}(G,a)). $$$

Lean4

/-- An orbit is a fixed block. -/
@[to_additive /-- An orbit is a fixed block. -/
    ]
protected theorem orbit (a : X) : IsFixedBlock G (orbit G a) :=
  (smul_orbit · a)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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