English
Let r be an element of a commutative semiring R and M an R-module. Then the ranges of the endomorphisms r^n id_M stabilize: there exists n such that for all m ≥ n, range(r^n id_M) = range(r^m id_M).
Русский
Пусть r ∈ R, и M — R-модуль. Тогда образы (range) эндоморфизмов r^n id_M стабилизируются: существует n, что для всех m ≥ n выполняется range(r^n id_M) = range(r^m id_M).
LaTeX
$$$ \\exists n\\in\\mathbb{N}, \\forall m \\ge n, \\operatorname{range}(r^n\\id_M) = \\operatorname{range}(r^m\\id_M). $$$
Lean4
theorem range_smul_pow_stabilizes (r : R) :
∃ n : ℕ,
∀ m,
n ≤ m →
LinearMap.range (r ^ n • LinearMap.id : M →ₗ[R] M) = LinearMap.range (r ^ m • LinearMap.id : M →ₗ[R] M) :=
monotone_stabilizes
⟨fun n => LinearMap.range (r ^ n • LinearMap.id : M →ₗ[R] M), fun n m h x ⟨y, hy⟩ =>
⟨r ^ (m - n) • y, by
dsimp at hy ⊢
rw [← smul_assoc, smul_eq_mul, ← pow_add, ← hy, add_tsub_cancel_of_le h]⟩⟩
