isInternal — Mathlib

English

The isInternal property for gradeBy asserts that the grading is internally realized as a direct sum inside the ambient algebra.

Русский

Свойство isInternal для gradeBy утверждает, что градация реализуется внутри алгебры как внутренняя сумма.

LaTeX

$$$\text{IsInternal}(\mathrm{gradeBy}\;R\;f)$$$

Lean4

/-- `AddMonoidAlgebra.gradeBy` describe an internally graded algebra. -/
theorem isInternal : DirectSum.IsInternal (gradeBy R f) :=
  DirectSum.Decomposition.isInternal _

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