pOrder — Mathlib

English

Equivalent characterizations of IsTorsion' for the submonoid of powers of p.

Русский

Эквивалентные характеристики IsTorsion' для подмоноида степеней p.

LaTeX

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

Lean4

/-- In a `p ^ ∞`-torsion module (that is, a module where all elements are cancelled by scalar
multiplication by some power of `p`), the smallest `n` such that `p ^ n • x = 0`. -/
def pOrder {p : R} (hM : IsTorsion' M <| Submonoid.powers p) (x : M) [∀ n : ℕ, Decidable (p ^ n • x = 0)] :=
  Nat.find <| (isTorsion'_powers_iff p).mp hM x

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