Invertible matrices over a ring with invariant basis number are square. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
matrix.square_of_invertible
{n : Type u_1}
{m : Type u_2}
[fintype n]
[decidable_eq n]
[fintype m]
[decidable_eq m]
{R : Type u_3}
[semiring R]
[invariant_basis_number R]
(M : matrix n m R)
(N : matrix m n R)
(h : M.mul N = 1)
(h' : N.mul M = 1) :