orbit_subgroup_one_eq_self

Mathlib.GroupTheory.Coset.Basic

URI: https://scilib.ai/kg/mathlib#orbit_subgroup_one_eq_self

English

The orbit of the identity element under s is s itself.

Русский

Орбита единицы под действием s равна самой подгруппе.

LaTeX

$$$\mathrm{Orb}_{s}(1) = s$$$

Lean4

@[to_additive]
theorem orbit_subgroup_one_eq_self : MulAction.orbit s (1 : α) = s :=
  orbit_subgroup_eq_self_of_mem s s.one_mem

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

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

Разделы

Аффилиация

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