smul_mem_iff

Mathlib.GroupTheory.GroupAction.SubMulAction

URI: https://scilib.ai/kg/mathlib#SubMulAction.smul_mem_iff

English

The orbit relation on p equals the comap of the ambient orbit relation via the inclusion.

Русский

Отношение орбит на p равно прообразу отношения орбит в M через включение.

LaTeX

$$$ MulAction.orbitRel\\ R\\ p = (MulAction.orbitRel\\ R\\ M).comap Subtype.val $$$

Lean4

theorem smul_mem_iff (s0 : s ≠ 0) : s • x ∈ p ↔ x ∈ p :=
  p.smul_mem_iff' (Units.mk0 s s0)

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

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

Разделы

Аффилиация

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