isTorsion'_powers_iff — Mathlib

English

Characterization of isTorsion' for submonoid of powers: a is torsion iff every x has finite power that kills it.

Русский

Характеризация: модуль IsTorsion' относительно подмножества степеней — это каждая точка имеет конечную степень, умножающую ее на ноль.

LaTeX

$$isTorsion'_powers_iff (p) : IsTorsion' M (Submonoid.powers p) ↔ ∀ x, ∃ n, p^n • x = 0$$

Lean4

theorem isTorsion'_powers_iff (p : R) : IsTorsion' M (Submonoid.powers p) ↔ ∀ x : M, ∃ n : ℕ, p ^ n • x = 0 :=
  by
  constructor
  · intro h x
    let ⟨⟨a, ⟨n, hn⟩⟩, hx⟩ := @h x
    dsimp at hn
    use n
    rw [hn]
    apply hx
  · intro h x
    let ⟨n, hn⟩ := h x
    exact ⟨⟨_, ⟨n, rfl⟩⟩, hn⟩

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