instIsStrictOrderedModuleRat — Mathlib

English

There is an order isomorphism between the Archimedean classes of M and those of DivisibleHull M.

Русский

Существует подпорядок-изоморфизм классов Архимедовых между $M$ и $DivisibleHull M$.

LaTeX

$$ArchimedeanClass Iso (M) ≃o ArchimedeanClass (DivisibleHull M)$$

Lean4

instance : IsStrictOrderedModule ℚ (DivisibleHull M)
    where
  smul_lt_smul_of_pos_left a ha b c
    h := by
    simp_rw [qsmul_of_nonneg ha.le]
    apply smul_lt_smul_of_pos_left h (by simpa using ha)
  smul_lt_smul_of_pos_right a ha b c
    h := by
    apply lt_of_sub_pos
    rw [← sub_smul]
    simp_rw [qsmul_of_nonneg (sub_pos_of_lt h).le]
    apply smul_pos (by simpa [← NNRat.coe_pos] using h) ha

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