Commit 2024-05-01 20:55 dfbbdde8

feat: make rank_mul_eq_left_of_isUnit_det into an effective simp lemma (#12244) These theorems give that if A is a unit, or a unitary, in the n x n matrices over a commutative ring R, and B is an m x n matrix over R, that multiplying B by A on the left or right doesn't change the rank of B. To facilitate this, added isUnits_det_units and det_isUnit lemmas.