package rocq-rouche-capelli

This package provides a formal proof of the Rouché–Capelli theorem (also known as the Kronecker–Capelli theorem) using the Rocq Prover and the Mathematical Components library. The theorem provides necessary and sufficient conditions for a system of linear equations to have solutions, stating that a system is consistent if and only if the rank of its coefficient matrix equals the rank of its augmented matrix.