English
Two Lex(HahnSeries Γ R) have equal ArchimedeanClass.mk iff their orderTop and leadingCoeff agree.
Русский
У двух Lex(HahnSeries Γ R) равны ArchimedeanClass.mk тогда и только тогда, когда их orderTop и leadingCoeff совпадают.
LaTeX
$$$ \\mathrm{archimedeanClassMk_eq_archimedeanClassMk_iff } {x y : \\mathrm{Lex} (\\mathrm{HahnSeries } \\ Γ \\ R)} : \\mathrm{ArchimedeanClass.mk } x = \\mathrm{ArchimedeanClass.mk } y \\\\iff (\\mathrm{orderTop}(\\mathrm{ofLex } x) = \\mathrm{orderTop}(\\mathrm{ofLex } y)) \\\\land (\\mathrm{ArchimedeanClass.mk }(\\mathrm{ofLex } x).leadingCoeff = \\mathrm{ArchimedeanClass.mk }(\\mathrm{ofLex } y).leadingCoeff) $$$
Lean4
/-- The correspondence between finite archimedean classes of `Lex (HahnSeries Γ R)`
and lexicographical pairs of `HahnSeries.orderTop` and the finite archimedean class of
`HahnSeries.leadingCoeff`. -/
noncomputable def finiteArchimedeanClassOrderIsoLex :
FiniteArchimedeanClass (Lex (HahnSeries Γ R)) ≃o Γ ×ₗ FiniteArchimedeanClass R :=
by
apply OrderIso.ofHomInv (finiteArchimedeanClassOrderHomLex Γ R) (finiteArchimedeanClassOrderHomInvLex Γ R)
· ext x
cases x with
| h x
obtain ⟨order, coeff⟩ := x
induction coeff using FiniteArchimedeanClass.ind with
| mk a ha
simp [finiteArchimedeanClassOrderHomLex, finiteArchimedeanClassOrderHomInvLex, ha]
· ext x
induction x using FiniteArchimedeanClass.ind with
| mk a ha
simp [finiteArchimedeanClassOrderHomLex, finiteArchimedeanClassOrderHomInvLex,
archimedeanClassMk_eq_archimedeanClassMk_iff, ha]
