smul — Mathlib

English

If c > 0 in a semifield and a is strictly positive, then c•a is strictly positive.

Русский

Если c > 0 в полуполю (полуполе) и a строго положительно, то c•a строго положительно.

LaTeX

$$$ c > 0 \\rightarrow (\\mathrm{IsStrictlyPositive}(a) \\rightarrow \\mathrm{IsStrictlyPositive}(c \\cdot a)) $$$

Lean4

@[grind ←, aesop safe apply]
protected theorem smul [Semifield 𝕜] [PartialOrder 𝕜] [Algebra 𝕜 A] [PosSMulMono 𝕜 A] {c : 𝕜} (hc : 0 < c) {a : A}
    (ha : IsStrictlyPositive a) : IsStrictlyPositive (c • a) :=
  by
  have hunit : IsUnit (c • a) := isUnit_iff_exists.mpr ⟨c⁻¹ • ha.isUnit.unit⁻¹, by simp [(ne_of_lt hc).symm]⟩
  exact hunit.isStrictlyPositive (smul_nonneg hc.le ha.nonneg)

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