mem_orbit_smul

Mathlib.GroupTheory.GroupAction.Defs

URI: https://scilib.ai/kg/mathlib#MulAction.mem_orbit_smul

English

If g ∈ G and a ∈ α, then g • a ∈ orbit G (a).

Русский

Если g ∈ G и a ∈ α, то g • a ∈ orbit G (a).

LaTeX

$$$$ g \\cdot a \\in \\operatorname{orbit}(G, a). $$$$

Lean4

@[to_additive]
theorem mem_orbit_smul (g : G) (a : α) : a ∈ orbit G (g • a) := by simp only [orbit_smul, mem_orbit_self]

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

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

Разделы

Аффилиация

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