instPosSMulStrictMono — Mathlib

English

The StarModule structure provides a strict monotonicity of smul when the scalar is positive.

Русский

Структура StarModule обеспечивает строгую монотонность умножения на положительный скаляр.

LaTeX

$$PosSMulStrictMono(R,A)$$

Lean4

instance : PosSMulStrictMono R A where
  smul_lt_smul_of_pos_left r hr a b
    hab := by
    rw [StarOrderedRing.pos_iff] at hr
    rw [StarOrderedRing.lt_iff] at hab ⊢
    obtain ⟨a, ha₀, ha, rfl⟩ := hab
    obtain ⟨hr₀, hr⟩ := hr
    exact ⟨r • a, smul_ne_zero hr₀ ha₀, smul_mem_closure_star_mul hr ha, smul_add ..⟩

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