divOf_zero

Mathlib.Algebra.MonoidAlgebra.Division

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

English

Dividing a sum by g equals the sum of the divisions by g.

Русский

Деление суммы на g равно сумме делений на g.

LaTeX

$$$$\frac{(x + y)}{\!\!\! /ᵒᶠ g} = \frac{x}{/ᵒᶠ g} + \frac{y}{ᵒᶠ g}.$$$$

Lean4

@[simp]
theorem divOf_zero (x : k[G]) : x /ᵒᶠ 0 = x := by
  ext
  simp only [AddMonoidAlgebra.divOf_apply, zero_add]

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

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

Разделы

Аффилиация

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