Theorems · Theorem · commutative algebra

Submodule.pow_pOrder_smul

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

Defined in

Mathlib.Algebra.Module.Torsion.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

MonoidAddCommMonoidDistribMulActionDecidable