Commit 2025-05-07 23:30 717d2de1

feat(Matrix/PosDef): decomposition into units (#24647) The main result here is PosDef A ↔ ∃ B : Matrix n n 𝕜, IsUnit B ∧ A = Bᴴ * B. This is the last equation in the matrix cookbook, and follows on from #8809. This also adds and cleans up a bunch of lemmas about Matrix.PosSemidef.sqrt in the process.