English
If M is a linear ordered additive group, then DivisibleHull M inherits a linear order compatible with its additive structure.
Русский
Если $M$ — линейно упорядоченная аддитивная группа, то DivisibleHull M наследует линейный порядок, совместимый с аддитивной структурой.
LaTeX
$$DivisibleHull M is a LinearOrder.$$
Lean4
instance : LinearOrder (DivisibleHull M)
where
le_refl
a :=
by
induction a with
| mk m s
simp
le_trans a b c hab
hbc :=
by
induction a with
| mk ma sa
induction b with
| mk mb sb
induction c with
| mk mc sc
rw [mk_le_mk] at ⊢ hab hbc
rw [← nsmul_le_nsmul_iff_right (show sb.val ≠ 0 by simp), smul_comm _ _ ma, smul_comm _ _ mc]
rw [← nsmul_le_nsmul_iff_right (show sc.val ≠ 0 by simp), smul_comm _ _ mb] at hab
rw [← nsmul_le_nsmul_iff_right (show sa.val ≠ 0 by simp)] at hbc
exact hab.trans hbc
le_antisymm a b h
h' :=
by
induction a with
| mk ma sa
induction b with
| mk mb sb
rw [mk_le_mk] at h h'
rw [mk_eq_mk_iff_smul_eq_smul]
exact le_antisymm h h'
le_total a
b :=
by
induction a with
| mk ma sa
induction b with
| mk mb sb
simp_rw [mk_le_mk]
exact le_total _ _
toDecidableLE := by
unfold DecidableLE LE.le instLE liftOn₂ LocalizedModule.liftOn₂
infer_instance
