exists_pow_succ_smul_dvd — Mathlib

English

For an Artinian module M over a commutative semiring R and r ∈ R, there exist n ∈ ℕ and y ∈ M such that r^{n+1} y = r^n x for a given x ∈ M.

Русский

Пусть M — артинановый модуль над коммутативным полем R, и r ∈ R, x ∈ M. Тогда существует n ∈ ℕ и y ∈ M such that r^{n+1} y = r^n x.

LaTeX

$$$ \\exists n\\in\\mathbb{N}, \\exists y\\in M, \\ r^{n+1} \\cdot y = r^n \\cdot x. $$$

Lean4

theorem exists_pow_succ_smul_dvd (r : R) (x : M) : ∃ (n : ℕ) (y : M), r ^ n.succ • y = r ^ n • x :=
  by
  obtain ⟨n, hn⟩ := IsArtinian.range_smul_pow_stabilizes M r
  simp_rw [SetLike.ext_iff] at hn
  exact ⟨n, by simpa using hn n.succ n.le_succ (r ^ n • x)⟩

Похожие утверждения