Theorems · Theorem · commutative algebra

Submodule.IsHomogeneous.mem_iff

∀ {ι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] {p : Submodule A M} (ℳ : ιM → σM) [inst_3 : DecidableEq ιM] [inst_4 : SetLike σM M]
  [inst_5 : AddSubmonoidClass σM M] [inst_6 : DirectSum.Decomposition ℳ],
  p.IsHomogeneous ℳ → ∀ {x : M}, x ∈ p ↔ ∀ (i : ιM), ↑(((DirectSum.decompose ℳ) x) i) ∈ p

Defined in

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEqSetLikeAddSubmonoidClassDirectSum.Decomposition