add_divOf

Mathlib.Algebra.MonoidAlgebra.Division

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

English

Addition distributes over division by g at the level of formal sums.

Русский

Суммирование распределяется через.divOf по g на уровне сумм.

LaTeX

$$$$ (x + y)/divOf g = x/divOf g + y/divOf g. $$$$

Lean4

theorem add_divOf (x y : k[G]) (g : G) : (x + y) /ᵒᶠ g = x /ᵒᶠ g + y /ᵒᶠ g :=
  map_add (Finsupp.comapDomain.addMonoidHom _) _ _

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

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

Разделы

Аффилиация

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