Theorems · Definition · commutative algebra

Submodule.pOrder

{R : Type u_1} →
  {M : Type u_2} →
    [inst : Monoid R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : DistribMulAction R M] →
          {p : R} → Module.IsTorsion' M ↥(Submonoid.powers p) → (x : M) → [(n : ℕ) → Decidable (p ^ n • x = 0)] → ℕ

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.

Defined in

Mathlib.Algebra.Module.Torsion.Basic

Cited by

7 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidAddCommMonoidDistribMulActionDecidable