Documentation

Mathlib.Data.Set.Pointwise.Iterate

Results about pointwise operations on sets with iteration. #

theorem vadd_eq_self_of_preimage_zsmul_eq_self {G : Type u_1} [AddCommGroup G] {n : } {s : Set G} (hs : (fun x => n x) ⁻¹' s = s) {g : G} {j : } (hg : 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.)

theorem smul_eq_self_of_preimage_zpow_eq_self {G : Type u_1} [CommGroup G] {n : } {s : Set G} (hs : (fun x => x ^ n) ⁻¹' s = s) {g : G} {j : } (hg : g ^ n ^ j = 1) :
g s = s

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