instIsStrictOrderedModuleOfIsCancelAdd

English

If x is nonzero and the ring is nontrivial, then star x times x is positive.

Русский

Если x не равно нулю и кольцо не тривиально, то star x умноженное на x положительно.

LaTeX

$$$ 0 < x^* x $$$

Lean4

instance [IsCancelAdd R] : IsStrictOrderedModule R A where
  smul_lt_smul_of_pos_right a ha r s
    hrs := by
    rw [StarOrderedRing.pos_iff] at ha
    rw [StarOrderedRing.lt_iff] at hrs ⊢
    obtain ⟨r, hr₀, hr, rfl⟩ := hrs
    obtain ⟨ha₀, ha⟩ := ha
    exact ⟨r • a, smul_ne_zero hr₀ ha₀, smul_mem_closure_star_mul hr ha, add_smul ..⟩

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