English
The symmetric image of ArchimedeanClass mk under the order isomorphism corresponds to the original class.
Русский
Симметрический образ ArchimedeanClass mk через порядок-изоморфизм соответствует исходному классу.
LaTeX
$$archimedeanClassOrderIso_symm_apply (m) (s) : (archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (DivisibleHull.mk m s)) = ArchimedeanClass.mk m$$
Lean4
/-- The Archimedean classes of `DivisibleHull M` are the same as those of `M`. -/
noncomputable def archimedeanClassOrderIso : ArchimedeanClass M ≃o ArchimedeanClass (DivisibleHull M) :=
by
apply OrderIso.ofHomInv (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M)
· ext a
induction a with
| mk a
induction a with
| mk m s
suffices ArchimedeanClass.mk (mk m 1) = ArchimedeanClass.mk (mk m s) by
simpa [archimedeanClassOrderHom, archimedeanClassOrderHomInv]
simp_rw [aux_archimedeanClassMk_mk]
· ext a
induction a with
| mk _
simp [archimedeanClassOrderHom, archimedeanClassOrderHomInv]
