Theorem LinearMap.singularValues_pos_iff_ne_zero

Modification history

2026-07-22 16:25
Mathlib/Analysis/InnerProductSpace/SingularValues.lean
style: fix by on newline (#41794) …
Modified LinearMap.singularValues_pos_iff_ne_zeroView on Github →
2026-03-23 22:20
Mathlib/Analysis/InnerProductSpace/SingularValues.lean
feat(Analysis/InnerProductSpace): definition of singular values for finite-dimensional inner product spaces (#33731) …
Added LinearMap.singularValues_pos_iff_ne_zeroView on Github →