modOf_apply_add_self

Mathlib.Algebra.MonoidAlgebra.Division

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

English

For any x, any g and any d, the coefficient of modOf g at g + d is zero.

Русский

Для любых x, g и d коэффициент modOf g в позиции g + d равен нулю.

LaTeX

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

Lean4

@[simp]
theorem modOf_apply_add_self (x : k[G]) (g : G) (d : G) : (x %ᵒᶠ g) (d + g) = 0 :=
  modOf_apply_of_exists_add _ _ _ ⟨_, add_comm _ _⟩

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

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

Разделы

Аффилиация

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