Theorems · Definition · commutative algebra

Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner

{R : Type u_1} →
  (M : Type u_3) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (r : R) → (rs : List R) → (M ⧸ Ideal.ofList (r :: rs) • ⊤) ≃ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs • ⊤

The equivalence between M ⧸ (r₀, r₁, …, rₙ)M and (M ⧸ r₀M) ⧸ (r₁, …, rₙ) (M ⧸ r₀M).

Defined in

Mathlib.RingTheory.Regular.RegularSequence

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule