orbit_eq_out_smul

Mathlib.GroupTheory.Coset.Basic

URI: https://scilib.ai/kg/mathlib#QuotientGroup.orbit_eq_out_smul

← MathLib Explorer

English

For x in α / s, the orbit of x equals x.out • s.

Русский

Для x в α / s орбита x равна x.out • s.

LaTeX

$$$\mathrm{orbit}(x) = x^{\mathrm{out}} \cdot s$$$

Lean4

@[to_additive]
theorem orbit_eq_out_smul (x : α ⧸ s) : MulAction.orbitRel.Quotient.orbit x = x.out • s :=
  by
  induction x using QuotientGroup.induction_on
  simp only [orbit_mk_eq_smul, ← eq_class_eq_leftCoset, Quotient.out_eq']

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

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

Разделы

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

Аффилиация

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