isPositive_natCast — Mathlib

English

For any natural n, the endomorphism n acting by scalar is positive.

Русский

Для любого естественного числа n отображение, умножающее на n, положительно.

LaTeX

$$$$\forall n \in \mathbb{N}, \; IsPositive(\text{ofNat}(n))$$$$

Lean4

@[simp]
theorem isPositive_natCast {n : ℕ} : IsPositive (n : E →ₗ[𝕜] E) :=
  by
  refine ⟨IsSymmetric.natCast n, fun x => ?_⟩
  simp only [Module.End.natCast_apply, ← Nat.cast_smul_eq_nsmul 𝕜, inner_smul_left, map_natCast, mul_re, natCast_re,
    inner_self_im, mul_zero, sub_zero]
  exact mul_nonneg n.cast_nonneg' inner_self_nonneg

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