IsHomogeneous — Mathlib

English

A submodule p ⊆ M is homogeneous if, whenever a vector lies in p, all its homogeneous components also lie in p.

Русский

Подмодуль p ⊆ M называется однородным, если для любого вектора из p все его однородные компоненты также лежат в p.

LaTeX

$$$$ \text{IsHomogeneous}(p, \mathcal{M}) \;\iff\; \forall x \in p, \forall i, (\mathrm{decompose} \mathcal{M} \, x \, i) \in p. $$$$

Lean4

/-- An `A`-submodule `p ⊆ M` is homogeneous if for every `m ∈ p`, all homogeneous components of `m` are
in `p`.
-/
def IsHomogeneous (p : Submodule A M) (ℳ : ιM → σM) [DecidableEq ιM] [SetLike σM M] [AddSubmonoidClass σM M]
    [Decomposition ℳ] : Prop :=
  SetLike.IsHomogeneous ℳ p

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