isInternal — Mathlib

English

The grade-by grading is internal to the direct-sum decomposition, i.e., isInternal holds for grade R.

Русский

Градация grade по ι является внутренней по отношению к разложению по прямой сумме.

LaTeX

$$$\mathrm{IsInternal}(\mathrm{grade}\;R)$$$

Lean4

/-- `AddMonoidAlgebra.grade` describe an internally graded algebra. -/
theorem isInternal : DirectSum.IsInternal (grade R : ι → Submodule R _) :=
  DirectSum.Decomposition.isInternal _

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