Theorems · Theorem · commutative algebra

Submodule.pOrder.congr_simp

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

Defined in

Mathlib.Algebra.Module.PID

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidAddCommMonoidDistribMulActionDecidable