English
Theorem le_def asserts the same characterisation as in the base order for elements of MulArchimedeanOrder M: a ≤ b iff ∃ n, |b| ≤ |a|^n.
Русский
Теорема le_def для MulArchimedeanOrder M повторяет характеристику неравенства: a ≤ b ⇔ ∃ n, |b| ≤ |a|^n.
LaTeX
$$$ a \le b \iff \exists n \in \mathbb{N}, \ |b| \le |a|^n $$$
Lean4
/-- An `OrderMonoidHom` can be made to an `OrderHom` between their `MulArchimedeanOrder`. -/
@[to_additive /-- An `OrderAddMonoidHom` can be made to an `OrderHom` between their
`ArchimedeanOrder`. -/
]
noncomputable def orderHom (f : M →*o N) : MulArchimedeanOrder M →o MulArchimedeanOrder N
where
toFun a := of (f a.val)
monotone' := by
rintro a b ⟨n, hn⟩
simp_rw [le_def, val_of, ← map_mabs, ← map_pow]
exact ⟨n, OrderHomClass.monotone f hn⟩
