English
Let x be a nonzero element of Lex(HahnSeries Γ, R). Then the second component of the image of the finite Archimedean class order isomorphism applied to the class of x coincides with the Archimedean class of the leading coefficient of x.
Русский
Пусть x непустой элемент в Lex(HahnSeries Γ, R). Тогда вторая компонента образа конечного изоморфа архимедианных классов под отображением, применяемым к классу x, совпадает с архимеданным классом ведущего коэффициента x.
LaTeX
$$$ (\mathrm{ofLex}(\mathrm{finiteArchimedeanClassOrderIsoLex}(\Gamma, R, \mathrm{FiniteArchimedeanClass.mk}(x, h)))).2.\mathrm{val} = \mathrm{ArchimedeanClass.mk}(\mathrm{ofLex}(x).leadingCoeff) $$$
Lean4
@[simp]
theorem finiteArchimedeanClassOrderIsoLex_apply_snd {x : Lex (HahnSeries Γ R)} (h : x ≠ 0) :
(ofLex (finiteArchimedeanClassOrderIsoLex Γ R (FiniteArchimedeanClass.mk x h))).2.val =
ArchimedeanClass.mk (ofLex x).leadingCoeff :=
by simp [finiteArchimedeanClassOrderIsoLex, finiteArchimedeanClassOrderHomLex]
