English
Let N be a commutative monoid with a M-action on N and IsScalarTower M N N. For r ∈ M and s ⊆ N, if x ∈ closure s, then there exists n ∈ ℕ such that r^n • x ∈ closure (r • s).
Русский
Пусть N — коммутативный моноид с действием M на N и т.н. тетраэдр-скаляров. Для r ∈ M и s ⊆ N, если x ∈ closure s, то существует n ∈ ℕ такое, что r^n • x ∈ closure (r • s).
LaTeX
$$$\\forall r \\in M,\\; s \\subseteq N,\\; x \\in \\operatorname{closure}(s)\\Rightarrow \\exists n \\in \\mathbb{N},\\; r^n \\cdot x \\in \\operatorname{closure}(r \\cdot s)$$$
Lean4
@[to_additive]
theorem pow_smul_mem_closure_smul {N : Type*} [CommMonoid N] [MulAction M N] [IsScalarTower M N N] (r : M) (s : Set N)
{x : N} (hx : x ∈ closure s) : ∃ n : ℕ, r ^ n • x ∈ closure (r • s) := by
induction hx using closure_induction with
| mem x hx => exact ⟨1, subset_closure ⟨_, hx, by rw [pow_one]⟩⟩
| one => exact ⟨0, by simp⟩
| mul x y _ _ hx hy =>
obtain ⟨⟨nx, hx⟩, ⟨ny, hy⟩⟩ := And.intro hx hy
use ny + nx
rw [pow_add, mul_smul, ← smul_mul_assoc, mul_comm, ← smul_mul_assoc]
exact mul_mem hy hx
