single_add

Mathlib.RingTheory.HahnSeries.Addition

URI: https://scilib.ai/kg/mathlib#HahnSeries.single_add

← MathLib Explorer

English

A consequence of linearity: the single map distributes over addition.

Русский

Следствие линейности: отображение single распределяется по сложению.

LaTeX

$$$$ \text{single}_a(r+s) = \text{single}_a(r) + \text{single}_a(s). $$$$

Lean4

@[simp]
theorem single_add (a : Γ) (r s : R) : single a (r + s) = single a r + single a s := by
  classical ext : 1; exact Pi.single_add (f := fun _ => R) a r s

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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