map_neg

Mathlib.RingTheory.HahnSeries.Addition

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

English

Negation commutes with coefficient maps: map f (-x) = -(map f x).

Русский

Отрицание коммутирует отображение коэффициентов: map f (-x) = -(map f x).

LaTeX

$$$$ ( -x ).map f = -\big( x.map f \big). $$$$

Lean4

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

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

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

Разделы

Аффилиация

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