Invertible matrices over a ring with invariant basis number are square.

theorem Matrix.square_of_invertible {n : Type u_1} {m : Type u_2} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] {R : Type u_3} [Semiring R] [InvariantBasisNumber R] (M : Matrix n m R) (N : Matrix m n R) (h : M * N = 1) (h' : N * M = 1) : Fintype.card n = Fintype.card m

@[instance 100]

instance rankCondition_of_nontrivial_of_commSemiring {R : Type u_4} [CommSemiring R] [Nontrivial R] : RankCondition R

Nontrivial commutative semirings R satisfy the rank condition.

If R is moreover a ring, then it satisfies the strong rank condition, see commRing_strongRankCondition. It is unclear whether this generalizes to semirings.