English
The support stays stable under the addOppositeEquiv operation.
Русский
Опора сохраняется при операции addOppositeEquiv.
LaTeX
$$$$ \operatorname{support}(\mathrm{addOppositeEquiv}(x)) = \operatorname{support}(x). $$$$
Lean4
/-- `addOppositeEquiv` is an additive monoid isomorphism between
Hahn series over `Γ` with coefficients in the opposite additive monoid `Rᵃᵒᵖ`
and the additive opposite of Hahn series over `Γ` with coefficients `R`.
-/
@[simps -isSimp]
def addOppositeEquiv : HahnSeries Γ Rᵃᵒᵖ ≃+ (HahnSeries Γ R)ᵃᵒᵖ
where
toFun x := .op ⟨fun a ↦ (x.coeff a).unop, by convert x.isPWO_support; ext; simp⟩
invFun x := ⟨fun a ↦ .op (x.unop.coeff a), by convert x.unop.isPWO_support; ext; simp⟩
left_inv x := by simp
right_inv
x := by
apply AddOpposite.unop_injective
simp
map_add' x
y := by
apply AddOpposite.unop_injective
ext
simp
