isHomogeneous — Mathlib

English

For a homogeneous submodule, the underlying submodule is homogeneous with respect to the given decomposition.

Русский

Для однородного подмодуля соответствующий подмодуль является однородным относительно заданной разложения.

LaTeX

$$$$ \text{Theorem}: p.toSubmodule.IsHomogeneous \mathcal{M}. $$$$

Lean4

theorem isHomogeneous (p : HomogeneousSubmodule 𝒜 ℳ) : p.toSubmodule.IsHomogeneous ℳ :=
  p.is_homogeneous'

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