Theorems · Definition · commutative algebra

Module.fgSystem.equiv

(R : Type u_1) →
  (M : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [inst_3 : DecidableEq (Submodule R M)] → Module.DirectLimit (fun i => ↥↑i) (Module.fgSystem R M) ≃ₗ[R] M

Every module is the direct limit of its finitely generated submodules.

Defined in

Mathlib.Algebra.Colimit.Finiteness

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEq