CoqEAL `rank` — matrix rank certified against `Matrix.rank` #

CoqEAL computes matrix rank by Gaussian elimination. This file certifies the base facts against Mathlib's Matrix.rank: the identity has full rank, and a diagonal of nonzero entries has full rank. The elimination-based general algorithm is the suite's frontier; here the refinement target — Matrix.rank — is pinned down on the cases where the answer is Fintype.card.