instMulArchimedean — Mathlib

English

If G is a commutative group with a linear order and is Archimedean in the sense of MulArchimedean, then the opposite order structure Gᵒᵈ is also MulArchimedean.

Русский

Если G — коммутативная группа с линейным порядком и обладает Архимедовым свойством в смысле MulArchimedean, то противоположный порядок Gᵒᵈ также обладает Архимедовым свойством.

LaTeX

$$$\\text{MulArchimedean}(G) \\Rightarrow \\text{MulArchimedean}(G^{\\mathrm{op}}).$$$

Lean4

@[to_additive]
instance instMulArchimedean [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] [MulArchimedean G] :
    MulArchimedean Gᵒᵈ :=
  ⟨fun x y hy =>
    let ⟨n, hn⟩ := MulArchimedean.arch (ofDual x)⁻¹ (inv_lt_one_iff_one_lt.2 hy)
    ⟨n, by rwa [inv_pow, inv_le_inv_iff] at hn⟩⟩

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