English
The Archimedean class of an element mk(m,s) in DivisibleHull M depends only on the numerator s, i.e., ArchimedeanClass.mk(mk(m,s)) = ArchimedeanClass.mk(mk(m,s')).
Русский
Архимедова часть элемента $\\mathrm{mk}(m,s)$ зависит только от числителя $s$; для любых $s,s'$ имеем равенство классов ArchimedeanClass.
LaTeX
$$ArchimedeanClass.mk(\\mathrm{mk}(m,s)) = ArchimedeanClass.mk(\\mathrm{mk}(m,s'))$$
Lean4
instance : IsStrictOrderedModule ℚ≥0 (DivisibleHull M)
where
smul_lt_smul_of_pos_left a ha b c
h :=
by
induction b with
| mk mb sb
induction c with
| mk mc sc
simp_rw [mk_lt_mk] at h
simp_rw [nnqsmul_mk, mk_lt_mk, smul_smul, PNat.mul_coe]
simp_rw [mul_right_comm _ _ a.num, mul_smul _ _ mc, mul_smul _ _ mb]
exact (nsmul_right_strictMono (by simpa using ha.ne.symm)).lt_iff_lt.mpr h
smul_lt_smul_of_pos_right a ha b c
h :=
by
induction a with
| mk m s
simp_rw [nnqsmul_mk, mk_lt_mk, smul_smul, PNat.mul_coe, PNat.mk_coe]
refine smul_lt_smul_of_pos_right ?_ ?_
· convert mul_lt_mul_of_pos_right (NNRat.lt_def.mp h) (show 0 < s.val by simp) using 1 <;> ring
· rw [← mk_zero 1, mk_lt_mk] at ha
simpa using ha
