smul_eq_self_of_mem_zpowers — Mathlib

English

If x ∈ zpowers y and y acts without moving a, then x also fixes a under the action.

Русский

Если x принадлежит zpowers y и y фиксирует a, то и x фиксирует a.

LaTeX

$$x ∈ Subgroup.zpowers y → (y • a = a) → (x • a = a)$$

Lean4

theorem smul_eq_self_of_mem_zpowers {α : Type*} [MulAction G α] (hx : x ∈ Subgroup.zpowers y) {a : α} (hs : y • a = a) :
    x • a = a := by
  obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp hx
  rw [← MulAction.toPerm_apply, ← MulAction.toPermHom_apply, MonoidHom.map_zpow _ y k, MulAction.toPermHom_apply]
  exact Function.IsFixedPt.perm_zpow (by exact hs) k

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