map_add

Mathlib.RingTheory.HahnSeries.Addition

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

← MathLib Explorer

English

The map f is additive: (x+y).map f = x.map f + y.map f (simp).

Русский

Отображение f аддитивно: (x+y).map f = x.map f + y.map f (упрощено).

LaTeX

$$$$ (x+y).map f = x.map f + y.map f. $$$$

Lean4

@[simp]
protected theorem map_add [AddMonoid S] (f : R →+ S) {x y : HahnSeries Γ R} :
    ((x + y).map f : HahnSeries Γ S) = x.map f + y.map f := by ext; simp

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

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

Разделы

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

Аффилиация

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