Theorems · Definition · commutative algebra

Submodule.IsHomogeneous

{ιM : Type u_2} →
  {σM : Type u_4} →
    {A : Type u_5} →
      {M : Type u_6} →
        [inst : Semiring A] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module A M] →
              Submodule A M →
                (ℳ : ιM → σM) →
                  [inst : DecidableEq ιM] →
                    [inst_3 : SetLike σM M] → [inst_4 : AddSubmonoidClass σM M] → [DirectSum.Decomposition ℳ] → Prop

An A-submodule p ⊆ M is homogeneous if for every m ∈ p, all homogeneous components of m are in p.

Defined in

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule

Cited by

8 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEqSetLikeAddSubmonoidClassDirectSum.Decomposition