Theorems · Theorem · commutative algebra

Submodule.CoFG.sInf_of_finite

∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherianRing R]
  {s : Set (Submodule R M)}, s.Finite → (∀ S ∈ s, S.CoFG) → (sInf s).CoFG

Over a noetherian ring the infimum of a finite family of CoFG submodules is CoFG.

Defined in

Mathlib.RingTheory.Finiteness.Cofinite

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleIsNoetherianRing