addOppositeEquiv_support

Mathlib.RingTheory.HahnSeries.Addition

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

← MathLib Explorer

English

The symmetric form preserves support via the inverse operation.

Русский

Симметрическая форма сохраняет опору через обращение.

LaTeX

$$$$ (addOppositeEquiv.symm x).support = x.unop.support. $$$$

Lean4

@[simp]
theorem addOppositeEquiv_support (x : HahnSeries Γ Rᵃᵒᵖ) : (addOppositeEquiv x).unop.support = x.support :=
  by
  ext
  simp [addOppositeEquiv_apply]

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

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

Разделы

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

Аффилиация

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