Problems of Linear Algebra

Stream: maths

[Hououin Kyouma]

Is there a theorem in mathlib stating that the dot product of vector x with itself equals the square of the magnitude of x? And does mathlib include relevant concepts and properties of positive semi-definite matrices?

[Jakub Nowak]

Maybe docs#real_inner_self_eq_norm_sq is what you need?

[Jakub Nowak]

@loogle "inner_self"

[loogle]

:search: InnerProductSpace.Core.ofReal_normSq_eq_inner_self, InnerProductSpace.Core.inner_self_of_eq_zero, and 38 more

[Jakub Nowak]

@loogle "inner_self", Norm

[loogle]

:search: CStarModule.norm_eq_sqrt_norm_inner_self, CStarModule.inner_self_nonneg, and 2 more

[Jakub Nowak]

@loogle "inner_self", "norm"

[loogle]

:search: InnerProductSpace.Core.ofReal_normSq_eq_inner_self, InnerProductSpace.Core.inner_self_eq_norm_mul_norm, and 8 more

[Jakub Nowak]

Jakub Nowak said:

loogle "inner_self", Norm

That should have been Norm.norm not Norm. :sweat_smile:

But the last query is probably better anyway.