smul_mem_orbit_smul

Mathlib.GroupTheory.GroupAction.Defs

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

English

For g,h ∈ G and a ∈ α, g • a ∈ orbit G (h • a).

Русский

Для g,h ∈ G и a ∈ α имеет место, что g • a ∈ orbit G (h • a).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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