pow_pOrder_smul — Mathlib

English

If M is torsion with respect to Submonoid.powers p, then p^pOrder(hM, x) acts as zero on x.

Русский

Если элемент x принадлежит которому-то торсионному подмодулю относительно степеней p, то p^pOrder действует нулём на x.

LaTeX

$$p ^ pOrder hM x • x = 0.$$

Lean4

@[simp]
theorem pow_pOrder_smul {p : R} (hM : IsTorsion' M <| Submonoid.powers p) (x : M) [∀ n : ℕ, Decidable (p ^ n • x = 0)] :
    p ^ pOrder hM x • x = 0 :=
  Nat.find_spec <| (isTorsion'_powers_iff p).mp hM x

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