IsHomogeneous

Mathlib.Algebra.DirectSum.Decomposition

URI: https://scilib.ai/kg/mathlib#DirectSum.SetLike.IsHomogeneous

Lean4

/-- A substructure `p ⊆ M` is homogeneous if for every `m ∈ p`, all homogeneous components
  of `m` are in `p`. -/
def IsHomogeneous {P : Type*} [SetLike P M] (p : P) : Prop :=
  ∀ (i : ι) ⦃m : M⦄, m ∈ p → (DirectSum.decompose ℳ m i : M) ∈ p

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru