GradedAlgebra — Mathlib

English

A special case of graded ring where the grading is by Submodule R A.

Русский

Особый случай градуированного кольца, когда градация задана через Submodule R A.

LaTeX

$$$\text{abbrev }\mathrm{GradedAlgebra} := \mathrm{GradedRing} \, 𝒜.$$$

Lean4

/-- A special case of `GradedRing` with `σ = Submodule R A`. This is useful both because it
can avoid typeclass search, and because it provides a more concise name. -/
abbrev GradedAlgebra :=
  GradedRing 𝒜

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