English
If there is an order-preserving isomorphism between two ordered monoids, Archimedean property is preserved from the first to the second.
Русский
Если существует упорядоченный изоморфизм между двумя упорядоченными моноидами, архимедово свойство сохраняется в обе стороны.
LaTeX
$$$(\text{e: } \alpha \cong_o \beta) \Rightarrow (\text{MulArchimedean } \alpha \Rightarrow \text{MulArchimedean } \beta)$$$
Lean4
@[to_additive]
theorem mulArchimedean {α β} [CommMonoid α] [PartialOrder α] [CommMonoid β] [PartialOrder β] (e : α ≃*o β)
[MulArchimedean α] : MulArchimedean β := by
constructor
intro x y hxy
replace hxy : 1 < e.symm y := by simp [← map_lt_map_iff e, hxy]
refine (MulArchimedean.arch (e.symm x) hxy).imp ?_
simp [← map_pow, ← map_le_map_iff e]
