instNeg

Mathlib.RingTheory.HahnSeries.Addition

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

Lean4

instance : Neg (HahnSeries Γ R) where
  neg
    x :=
    { coeff := fun a => -x.coeff a
      isPWO_support' := by
        rw [Function.support_fun_neg]
        exact x.isPWO_support }

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

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

Разделы

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

Аффилиация

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