Theorems · Theorem · commutative algebra

Module.Finite.of_localized_maximal

∀ {R : Type u_1} [inst : CommSemiring R] [Finite (MaximalSpectrum R)] (M : Type u_2) [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M],
  (∀ (P : Ideal R) [inst_4 : P.IsMaximal], Module.Finite (Localization P.primeCompl) (LocalizedModule P.primeCompl M)) →
    Module.Finite R M

Defined in

Mathlib.RingTheory.LocalProperties.Semilocal

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringFiniteAddCommMonoidModule