Theorems · Definition · commutative algebra

Submodule.factorPow

{R : Type u_1} →
  [inst : Ring R] →
    (I : Ideal R) →
      (M : Type u_2) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {m n : ℕ} → m ≤ n → M ⧸ I ^ n • ⊤ →ₗ[R] M ⧸ I ^ m • ⊤

The linear map from M ⧸ I ^ m • ⊤ to M ⧸ I ^ n • ⊤ induced by the natural inclusion I ^ n • ⊤ → I ^ m • ⊤. To future contributors: Before adding lemmas related to Submodule.factorPow, please check whether it can be generalized to Submodule.factor and whether the corresponding (more general) lemma for Submodule.factor already exists.

Defined in

Mathlib.RingTheory.Ideal.Quotient.PowTransition

Cited by

17 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModule