isPosSemidef_zero — Mathlib

English

The zero bilinear form is positive semidefinite; it is symmetric and nonnegative.

Русский

Нулевая билинейная форма положительно полусобственна; она симметрична и неотрицательна.

LaTeX

$$$\text{IsPosSemidef}(0)=\text{true}$ (with $\text{isSymm}=\text{isSymm_zero}$ and $\text{isNonneg}=\text{isNonneg_zero}$).$$

Lean4

@[simp]
theorem isPosSemidef_zero [Preorder R] : IsPosSemidef (0 : M →ₛₗ[I₁] M →ₗ[R] R)
    where
  isSymm := isSymm_zero
  isNonneg := isNonneg_zero

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