A Unified Framework for Formalizing Matrix Decomposition Proofs

Wanli Ma, Zichen Wang, Zaiwen Wen

Existence proofs for many matrix decompositions share a recursive routine: a local transformation prepares the matrix, a slice is selected, a recursive solution is obtained, and th…