linMulLinSelfPosDef — Mathlib

English

If a linear map f has trivial kernel, then the quadratic form Q(x) = f(x)^2 is positive definite.

Русский

Если линейное отображение f инъективно, то квадратичная форма Q(x) = f(x)^2 положительно определена.

LaTeX

$$$\ker f = \{0\} \Rightarrow \operatorname{PosDef}(\mathrm{linMulLin}(f,f))$$$

Lean4

theorem linMulLinSelfPosDef {R} [CommSemiring R] [Module R M] [Semiring A] [LinearOrder A] [IsStrictOrderedRing A]
    [ExistsAddOfLE A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (f : M →ₗ[R] A)
    (hf : LinearMap.ker f = ⊥) : PosDef (linMulLin (A := A) f f) := fun _x hx =>
  mul_self_pos.2 fun h => hx <| LinearMap.ker_eq_bot'.mp hf _ h

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