modOf_apply_self_add

Mathlib.Algebra.MonoidAlgebra.Division

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

English

The same as above: the remainder vanishes on sums with g.

Русский

То же самое: остаток равен нулю на сумме с g.

LaTeX

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

Lean4

theorem modOf_apply_self_add (x : k[G]) (g : G) (d : G) : (x %ᵒᶠ g) (g + d) = 0 :=
  modOf_apply_of_exists_add _ _ _ ⟨_, rfl⟩

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

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

Разделы

Аффилиация

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