isStrictlyPositive_algebraMap — Mathlib

English

If c > 0 in the scalar field, then algebraMap c is strictly positive.

Русский

Если c > 0 в скалярном поле, тогда algebraMap c строго положительный.

LaTeX

$$$ 0 < c \\rightarrow \\mathrm{IsStrictlyPositive}(\\mathrm{algebraMap}_{\\mathbb{k},A}(c)) $$$

Lean4

@[grind ←, aesop safe apply]
theorem _root_.isStrictlyPositive_algebraMap [ZeroLEOneClass A] [Semifield 𝕜] [PartialOrder 𝕜] [Algebra 𝕜 A]
    [PosSMulMono 𝕜 A] {c : 𝕜} (hc : 0 < c) : IsStrictlyPositive (algebraMap 𝕜 A c) :=
  by
  rw [Algebra.algebraMap_eq_smul_one]
  exact IsStrictlyPositive.smul hc isStrictlyPositive_one

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