English
Let x be an element of the additive opposite Hahn series; then the leading coefficient of its inverse-opposite realization equals the opposite of the leading coefficient of the original series.
Русский
Пусть x принадлежит HahnSeries с противоположной структурой; тогда ведущий коэффициент образовавшегося при применении обратного отображения противоположности ряда равен противоположному ведущему коэффициенту исходного ряда.
LaTeX
$$$$ \operatorname{leadingCoeff}\left( \operatorname{addOppositeEquiv}^{-1}(x) \right) = \operatorname{op}\left( \operatorname{leadingCoeff}\left( \operatorname{unop}(x) \right) \right). $$$$
Lean4
@[simp]
theorem addOppositeEquiv_symm_leadingCoeff (x : (HahnSeries Γ R)ᵃᵒᵖ) :
(addOppositeEquiv.symm x).leadingCoeff = .op x.unop.leadingCoeff :=
by
apply AddOpposite.unop_injective
rw [← addOppositeEquiv_leadingCoeff, AddEquiv.apply_symm_apply, AddOpposite.unop_op]
