feat(Analysis/Normed/Operator): definition of singular values for linear maps#32126

Draft

nielsvoss wants to merge 11 commits intoleanprover-community:masterfrom

RanadeLabBerkeley:SingularValues

Commits on Oct 9, 2025

this is the initial commit with our singular value definitions and tsupporting theorems with sorries. It is under Mathlib/LinearAlgebra/SingularValues.lean
arnavmehtayy
committed

Commits on Nov 26, 2025

Merge branch 'leanprover-community:master' into SingularValues
nielsvoss
authored

Commits on Nov 28, 2025

More work on proving existence theorem
nielsvoss
committed