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)
: