Theorems · Definition · commutative algebra

Ideal.Filtration.submodule

{R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {I : Ideal R} → I.Filtration M → Submodule (↥(reesAlgebra I)) (PolynomialModule R M)

The R[IX]-submodule of M[X] associated with an I-filtration.

Defined in: Mathlib.RingTheory.Filtration
Cited by: 7 results in Mathlib
Foundations: Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing AddCommGroup Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Modulestatement and proof · cited by 20,661
CommRingstatement and proof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
Submodulestatement · cited by 7,192
Set.ofPredproof · cited by 6,101
Polynomialstatement and proof · cited by 5,681
Idealstatement and proof · cited by 4,748
Subalgebrastatement · cited by 1,353
PolynomialModulestatement and proof · cited by 76
Ideal.Filtrationstatement and proof · cited by 32
Ideal.Filtration.Nproof · cited by 29

Cited by8

Results whose statement or proof uses this declaration.

Ideal.Filtration.Stable.of_leproof · cited by 2
Ideal.Filtration.submodule_span_singlestatement and proof · cited by 2
Ideal.Filtration.submoduleInfHomproof · cited by 1
Ideal.Filtration.submodule_closure_singlestatement and proof · cited by 1
Ideal.Filtration.submodule_eq_span_le_iff_stable_gestatement · cited by 1
Ideal.Filtration.submodule_fg_iff_stablestatement and proof · cited by 1
Ideal.Filtration.mem_submodulestatement · cited by 0
Ideal.Filtration.inf_submodulestatement · cited by 0