finiteArchimedeanClassOrderIso_apply

English

For a nonzero x, the Archimedean class order is sent to the leading coefficient via the Lex embedding, i.e., finiteArchimedeanClassOrderIsoΓR applied to x class equals the orderTop of ofLex x.

Русский

Для непустого x архимедановый класс отображается в ведущий коэффициент через лексическое вложение: применённый к классу x образ отображения Arch немедленно даёт orderTop(ofLex x).

LaTeX

$$$\mathrm{finiteArchimedeanClassOrderIso}(\Gamma, R)(\mathrm{FiniteArchimedeanClass.mk}(x, h)) = (\mathrm{ofLex}(x)).\mathrm{orderTop}$$$

Lean4

@[simp]
theorem finiteArchimedeanClassOrderIso_apply {x : Lex (HahnSeries Γ R)} (h : x ≠ 0) :
    finiteArchimedeanClassOrderIso Γ R (FiniteArchimedeanClass.mk x h) = (ofLex x).orderTop := by
  simp [finiteArchimedeanClassOrderIso]

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