divOf_add

Mathlib.Algebra.MonoidAlgebra.Division

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

English

Another formulation of addDivOf: division distributes over addition.

Русский

Ещё одно формулирование: деление распределяется по сложению.

LaTeX

$$$$ x/ᵒᶠ g + y/ᵒᶠ g = (x+y)/ᵒᶠ g. $$$$

Lean4

theorem divOf_add (x : k[G]) (a b : G) : x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b :=
  by
  ext
  simp only [AddMonoidAlgebra.divOf_apply, add_assoc]

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

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

Разделы

Аффилиация

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