Theorems · Theorem · dynamical systems

vadd_eq_self_of_preimage_zsmul_eq_self

∀ {G : Type u_1} [inst : AddCommGroup G] {n : ℤ} {s : Set G},
  (fun x => n • x) ⁻¹' s = s → ∀ {g : G} {j : ℕ}, n ^ j • g = 0 → g +ᵥ s = s

Let n : ℤ and s a subset of an additive commutative group G that is invariant under preimage for the map x ↦ n • x. Then s is invariant under the pointwise action of the additive subgroup of elements g : G such that (n^j) • g = 0 for some j : ℕ. (This additive subgroup is called the Prüfer subgroup when G is the AddCircle and n is prime.)

Defined in

Mathlib.Dynamics.FixedPoints.Prufer

Cited by

1 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroup