gradeBy_id

Mathlib.Algebra.MonoidAlgebra.Grading

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

English

The remainder of x by g vanishes at any place of the form d + g.

Русский

Остаток по g равен нулю в позициях вида d + g.

LaTeX

$$$ (x \\bmod^{\\circ} g) (d + g) = 0 $$$

Lean4

theorem gradeBy_id : gradeBy R (id : M → M) = grade R :=
  rfl

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

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

Разделы

Аффилиация

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