Results about pointwise operations on sets with iteration. #
theorem
smul_eq_self_of_preimage_zpow_eq_self
{G : Type u_1}
[CommGroup G]
{n : ℤ}
{s : Set G}
(hs : (fun (x : G) => x ^ n) ⁻¹' s = s)
{g : G}
{j : ℕ}
(hg : g ^ n ^ j = 1)
:
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.)
theorem
vadd_eq_self_of_preimage_zsmul_eq_self
{G : Type u_1}
[AddCommGroup G]
{n : ℤ}
{s : Set G}
(hs : (fun (x : G) => n • x) ⁻¹' s = s)
{g : G}
{j : ℕ}
(hg : n ^ j • g = 0)
:
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.)