le_stabilizer_smul_right — Mathlib

English

If an element h fixes b under a larger group action, then h fixes a·b under the same compatible action.

Русский

Если элемент h фиксирует b под большими условиями действия, тогда он фиксирует a·b под тем же совместимым действием.

LaTeX

$$$stabilizer\;G'\ b\subseteq stabilizer\;G'\ (a\cdot b)$$$

Lean4

@[to_additive]
theorem le_stabilizer_smul_right {G'} [Group G'] [SMul α β] [MulAction G' β] [SMulCommClass G' α β] (a : α) (b : β) :
    stabilizer G' b ≤ stabilizer G' (a • b) := by simp_rw [SetLike.le_def, mem_stabilizer_iff, smul_comm]; rintro a h;
  rw [h]

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