grade

Mathlib.Algebra.MonoidAlgebra.Grading

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.grade

English

The remainder coeffs are preserved away from cosets g + d when there is no such coset.

Русский

Коэффициенты остатка сохраняются вне косетов г + d, если такого косета не существует.

LaTeX

$$$ (x \\bmod^{\\circ} g)_{g'} = x_{g'} \\quad\\text{if no } \\exists d, g' = g + d$$$

Lean4

/-- The submodule corresponding to each grade. -/
abbrev grade (m : M) : Submodule R R[M] :=
  gradeBy R id m

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru