English
The scalar action of a star-ordered ring on a module is order-preserving with the appropriate nonnegativity conditions.
Русский
Действие скаляр на модуле над звёздно упорядоченным кольцом сохраняет порядок при соответствующих условиях неотрицательности.
LaTeX
$$IsOrderedModule(R,A)$$
Lean4
instance : IsOrderedModule R A
where
smul_le_smul_of_nonneg_left r hr a b
hab := by
rw [StarOrderedRing.nonneg_iff] at hr
rw [StarOrderedRing.le_iff] at hab ⊢
obtain ⟨a, ha, rfl⟩ := hab
exact ⟨r • a, smul_mem_closure_star_mul hr ha, smul_add ..⟩
smul_le_smul_of_nonneg_right a ha r s
hrs := by
rw [StarOrderedRing.nonneg_iff] at ha
rw [StarOrderedRing.le_iff] at hrs ⊢
obtain ⟨r, hr, rfl⟩ := hrs
exact ⟨r • a, smul_mem_closure_star_mul hr ha, add_smul ..⟩
