orderTop_neg

Mathlib.RingTheory.HahnSeries.Addition

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

English

Negation preserves orderTop: orderTop(-x) = orderTop(x).

Русский

Отрицание сохраняет orderTop: orderTop(-x) = orderTop(x).

LaTeX

$$$$ \operatorname{orderTop}(-x) = \operatorname{orderTop}(x). $$$$

Lean4

@[simp]
theorem orderTop_neg {x : HahnSeries Γ R} : (-x).orderTop = x.orderTop := by
  classical simp only [orderTop, support_neg, neg_eq_zero]

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

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

Разделы

Аффилиация

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